src/Doc/Datatypes/Datatypes.thy

 
 \item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive
 Functions,'' describes how to specify corecursive functions using the
 @{command primcorec} and @{command primcorecursive} commands.
 
-\item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
+\item Section \ref{sec:introducing-bounded-natural-functors}, ``Introducing
 Bounded Natural Functors,'' explains how to use the @{command bnf} command
 to register arbitrary type constructors as BNFs.
 
 \item Section
 \ref{sec:deriving-destructors-and-theorems-for-free-constructors},

 @{typ 'b} is live.
 
 Type constructors must be registered as BNFs to have live arguments. This is
 done automatically for datatypes and codatatypes introduced by the @{command
 datatype_new} and @{command codatatype} commands.
-Section~\ref{sec:registering-bounded-natural-functors} explains how to register
-arbitrary type constructors as BNFs.
+Section~\ref{sec:introducing-bounded-natural-functors} explains how to
+register arbitrary type constructors as BNFs.
 
 Here is another example that fails:
 *}
 
     datatype_new 'a pow_list = PNil 'a (*<*)'a
     datatype_new 'a pow_list' = PNil' 'a (*>*)| PCons "('a * 'a) pow_list"
 
 text {*
 \noindent
-This one features a different flavor of nesting, where the recursive call in the
-type specification occurs around (rather than inside) another type constructor.
+This attempted definition features a different flavor of nesting, where the
+recursive call in the type specification occurs around (rather than inside)
+another type constructor.
 *}
 
 subsubsection {* Auxiliary Constants and Properties
   \label{sssec:datatype-auxiliary-constants-and-properties} *}
 

       null: Nil (defaults tl: Nil)
     | Cons (hd: 'a) (tl: "'a list")
 
 text {*
 \noindent
+The introduced constants are listed below.
+
+\medskip
 
 \begin{tabular}{@ {}ll@ {}}
 Constructors: &
   @{text "Nil \<Colon> 'a list"} \\
 &

   @{text "map \<Colon> ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"} \\
 Relator: &
   @{text "list_all2 \<Colon> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool"}
 \end{tabular}
 
+\medskip
+
 The discriminator @{const null} and the selectors @{const hd} and @{const tl}
-are characterized as follows:
+are characterized by the following conditional equations:
 %
 \[@{thm list.collapse(1)[of xs, no_vars]}
   \qquad @{thm list.collapse(2)[of xs, no_vars]}\]
 %
 For two-constructor datatypes, a single discriminator constant is sufficient.

     (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
   ;
   @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')'
 \<close>}
 
+\medskip
+
+\noindent
 The syntactic entity \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}.
 %
 The optional target is potentially followed by datatype-specific options:

   @{syntax_def tyargs}: typefree | '(' ((name ':')? typefree + ',') ')'
   ;
   @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
 \<close>}
 
+\medskip
+
 \noindent
 The syntactic entity \synt{name} denotes an identifier, \synt{typefree}
 denotes fixed type variable (@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix}
 denotes the usual parenthesized mixfix notation. They are documented in the Isar
 reference manual \cite{isabelle-isar-ref}.

 constructors as long as they share the same type.
 
 @{rail \<open>
   @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')'
 \<close>}
+
+\medskip
 
 \noindent
 Given a constructor
 @{text "C \<Colon> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<sigma>"},
 default values can be specified for any selector

 
 @{rail \<open>
   @@{command datatype_new_compat} names
 \<close>}
 
-\noindent
-The old datatype package provides some functionality that is not yet replicated
-in the new package:
+\medskip
+
+\noindent
+The old datatype package provides some functionality that is not yet
+replicated in the new package:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}
 
 \item It is integrated with \keyw{fun} and \keyw{function}

 
 In the other direction, there is currently no way to register old-style
 datatypes as new-style datatypes. If the goal is to define new-style datatypes
 with nested recursion through old-style datatypes, the old-style
 datatypes can be registered as a BNF
-(Section~\ref{sec:registering-bounded-natural-functors}). If the goal is
+(Section~\ref{sec:introducing-bounded-natural-functors}). If the goal is
 to derive discriminators and selectors, this can be achieved using @{command
 wrap_free_constructors}
 (Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
 *}
 

 @{rail \<open>
   @@{command codatatype} target? \<newline>
     (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
 \<close>}
 
+\medskip
+
 \noindent
 Definitions of codatatypes have almost exactly the same syntax as for datatypes
 (Section~\ref{ssec:datatype-command-syntax}). The @{text "no_discs_sels"} option
 is not available, because destructors are a crucial notion for codatatypes.
 *}

   @{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')'
   ;
   @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
 \<close>}
 
+\medskip
+
+\noindent
 The optional target is potentially followed by a corecursion-specific option:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}
 

 partial_function to the rescue
 *}
 *)
 
 
-section {* Registering Bounded Natural Functors
-  \label{sec:registering-bounded-natural-functors} *}
+section {* Introducing Bounded Natural Functors
+  \label{sec:introducing-bounded-natural-functors} *}
 
 text {*
 The (co)datatype package can be set up to allow nested recursion through
 arbitrary type constructors, as long as they adhere to the BNF requirements
 and are registered as BNFs. It is also possible to declare a BNF abstractly

   @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
   ;
   @{syntax_def wit_types}: '[' 'wits' ':' types ']'
 \<close>}
 
+\medskip
+
 \noindent
 The @{command bnf_decl} command declares a new type and associated constants
 (map, set, relator, and cardinal bound) and asserts the BNF properties for
 these constants as axioms. Type arguments are live by default; they can be
-marked as dead by entering \texttt{-} (hyphen) instead of a name for the
+marked as dead by entering ``-'' (hyphen) instead of an identifier for the
 corresponding set function. Witnesses can be specified by their types.
 Otherwise, the syntax of @{command bnf_decl} is
 identical to the left-hand side of a @{command datatype_new} or @{command
 codatatype} definition.
 

   ;
   @{syntax_def name_term}: (name ':' term)
   ;
   X_list: '[' (X + ',') ']'
 \<close>}
+
+\medskip
 
 % options: no_discs_sels no_code rep_compat
 
 \noindent
 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.