src/Doc/Datatypes/Datatypes.thy

 Tutorial for (co)datatype definitions with the new package.
 *)
 
 theory Datatypes
 imports Setup
+keywords
+  "primrec_new" :: thy_decl and
+  "primcorec" :: thy_decl
 begin
 
-(*
-text {*
-
-  primrec_new <fixes>
-
-*}
-*)
+(*<*)
+(* FIXME: Evil setup until "primrec_new" and "primcorec" are in place. *)
+ML_command {*
+fun add_dummy_cmd _ _ lthy = lthy;
+
+val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"} ""
+  (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd);
+
+val _ = Outer_Syntax.local_theory @{command_spec "primcorec"} ""
+  (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd);
+*}
+(*>*)
+
 
 section {* Introduction
   \label{sec:introduction} *}
 
 text {*
 The 2013 edition of Isabelle introduced new definitional package for datatypes
 and codatatypes. The datatype support is similar to that provided by the earlier
 package due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL},
 documented in the Isar reference manual \cite{isabelle-isar-ref};
-indeed, replacing @{command datatype} by @{command datatype_new} is usually
-sufficient to port existing specifications to the new package. What makes the
-new package attractive is that it supports definitions with recursion through a
-large class of non-datatypes, notably finite sets:
-*}
-
-    datatype_new 'a treeFS = TreeFS 'a "'a treeFS fset"
-
-text {*
-\noindent
-Another advantage of the new package is that it supports local definitions:
+indeed, replacing the keyword @{command datatype} by @{command datatype_new} is
+usually all that is needed to port existing theories to use the new package.
+
+Perhaps the main advantage of the new package is that it supports definitions
+with recursion through a large class of non-datatypes, notably finite sets:
+*}
+
+    datatype_new 'a treeFS = NodeFS 'a "'a treeFS fset"
+
+text {*
+\noindent
+Another strong point is that the package supports local definitions:
 *}
 
     context linorder
     begin
       datatype_new flag = Less | Eq | Greater
     end
 
 text {*
 \noindent
-Finally, the package also provides some convenience, notably automatically
-generated destructors.
-
-The command @{command datatype_new} is expected to displace @{command datatype} in a future
-release. Authors of new theories are encouraged to use @{command datatype_new}, and
-maintainers of older theories may want to consider upgrading in the coming months.
-
-The package also provides codatatypes (or ``coinductive datatypes''), which may
-have infinite values. The following command introduces a codatatype of infinite
-streams:
+The package also provides some convenience, notably automatically generated
+destructors.
+
+The command @{command datatype_new} is expected to displace @{command datatype}
+in a future release. Authors of new theories are encouraged to use
+@{command datatype_new}, and maintainers of older theories may want to consider
+upgrading in the coming months.
+
+In addition to plain inductive datatypes, the package supports coinductive
+datatypes, or \emph{codatatypes}, which may have infinite values. For example,
+the following command introduces a codatatype of infinite streams:
 *}
 
     codatatype 'a stream = Stream 'a "'a stream"
 
 text {*
 \noindent
-Mixed inductive--coinductive recursion is possible via nesting.
-Compare the following four examples:
-*}
-
-    datatype_new 'a treeFF = TreeFF 'a "'a treeFF list"
-    datatype_new 'a treeFI = TreeFI 'a "'a treeFF stream"
-    codatatype 'a treeIF = TreeIF 'a "'a treeFF list"
-    codatatype 'a treeII = TreeII 'a "'a treeFF stream"
-
-text {*
+Mixed inductive--coinductive recursion is possible via nesting. Compare the
+following four examples:
+*}
+
+    datatype_new 'a treeFF = NodeFF 'a "'a treeFF list"
+    datatype_new 'a treeFI = NodeFI 'a "'a treeFF stream"
+    codatatype 'a treeIF = NodeIF 'a "'a treeFF list"
+    codatatype 'a treeII = NodeII 'a "'a treeFF stream"
+
+text {*
+The first two tree types allow only finite branches, whereas the last two allow
+infinite branches. Orthogonally, the nodes in the first and third types have
+finite branching, whereas those of the second and fourth have infinitely many
+direct subtrees.
+
 To use the package, it is necessary to import the @{theory BNF} theory, which
 can be precompiled as the \textit{HOL-BNF} image. The following commands show
 how to launch jEdit/PIDE with the image loaded and how to build the image
 without launching jEdit:
 *}

 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} *}
+subsection {* Examples
+  \label{ssec:datatype-examples} *}
 
 subsubsection {* Nonrecursive Types *}
 
 text {*
 enumeration type:

 
 More complex example, which reuses our maybe and triple types:
 *}
 
     datatype_new 'a triple_tree =
-      Triple_Tree "('a triple_tree maybe, bool, 'a triple_tree maybe) triple"
+      Triple_Node "('a triple_tree maybe, bool, 'a triple_tree maybe) triple"
 
 text {*
 Recursion may not be arbitrary; e.g. impossible to define
 *}
 

     datatype_new (set_: 'a) list_ =
       null: Nil ("[]")
     | Cons (hd: 'a) (tl: "'a list_") (infixr "#" 65)
 
 
-subsection {* General Syntax
-  \label{ssec:datatype-general-syntax} *}
+subsection {* Syntax
+  \label{ssec:datatype-syntax} *}
 
 text {*
 Datatype definitions have the following general syntax:
 
 @{rail "

 names of the set functions (@{text t_set1}, \ldots, @{text t_setM}).
 Inside a mutually recursive datatype specification, all defined datatypes must
 specify exactly the same type variables in the same order.
 
 @{rail "
-  @{syntax_def ctor}: (@{syntax name} ':')? @{syntax name} (@{syntax ctor_arg} *) \\
+  @{syntax_def ctor}: (@{syntax name} ':')? @{syntax name} (@{syntax ctor_arg} * ) \\
     @{syntax sel_defaults}? @{syntax mixfix}?
 "}
 
 \noindent
 The main constituents of a constructor specification is the name of the

 associated with other constructors. The specified default value must have type
 @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<tau>"}
 (i.e., it may dependend on @{text C}'s arguments).
 *}
 
-subsection {* Characteristic Theorems
-  \label{ssec:datatype-characteristic-theorems} *}
+subsection {* Generated Theorems
+  \label{ssec:datatype-generated-theorems} *}
 
 text {*
   * free ctor theorems
     * case syntax
 

 
 text {*
 More examples in \verb|~~/src/HOL/BNF/Examples|.
 *}
 
-subsection {* Introductory Examples
-  \label{ssec:primrec-introductory-examples} *}
+subsection {* Examples
+  \label{ssec:primrec-examples} *}
 
 subsubsection {* Nonrecursive Types *}
 
 
 subsubsection {* Simple Recursion *}

 
 
 subsubsection {* Nested-as-Mutual Recursion *}
 
 
-subsection {* General Syntax
-  \label{ssec:primrec-general-syntax} *}
-
-text {*
-
-*}
-
-subsection {* Characteristic Theorems
-  \label{ssec:primrec-characteristic-theorems} *}
+subsection {* Syntax
+  \label{ssec:primrec-syntax} *}
+
+text {*
+Primitive recursive functions have the following general syntax:
+
+@{rail "
+  @@{command primrec_new} @{syntax target}? @{syntax \"fixes\"} \\ @'where'
+    (@{syntax primrec_equation} + '|')
+  ;
+  @{syntax_def primrec_equation}: @{syntax thmdecl}? @{syntax prop}
+"}
+*}
+
+
+subsection {* Generated Theorems
+  \label{ssec:primrec-generated-theorems} *}
 
 text {*
   * synthesized nonrecursive definition
   * user specification is rederived from it, exactly as entered
 

     * without some needless induction hypotheses if not used
   * fold, rec
     * mutualized
 *}
 
-subsection {* Recursive Default Values
-  \label{ssec:recursive-default-values} *}
+subsection {* Recursive Default Values for Selectors
+  \label{ssec: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

 This section describes how to specify codatatypes using the @{command codatatype}
 command.
 *}
 
 
-subsection {* Introductory Examples
-  \label{ssec:codatatype-introductory-examples} *}
+subsection {* Examples
+  \label{ssec:codatatype-examples} *}
 
 text {*
 More examples in \verb|~~/src/HOL/BNF/Examples|.
 *}
 
 
-subsection {* General Syntax
-  \label{ssec:codatatype-general-syntax} *}
+subsection {* Syntax
+  \label{ssec:codatatype-syntax} *}
 
 text {*
 Definitions of codatatypes have almost exactly the same syntax as for datatypes
-(Section~\ref{ssec:datatype-general-syntax}), with two exceptions: The command
-is called @{command codatatype}; the \keyw{no\_dests} option is not
-available, because destructors are a central notion for codatatypes.
-*}
-
-subsection {* Characteristic Theorems
-  \label{ssec:codatatype-characteristic-theorems} *}
+(Section~\ref{ssec:datatype-syntax}), with two exceptions: The command is called
+@{command codatatype}; the \keyw{no\_dests} option is not available, because
+destructors are a central notion for codatatypes.
+*}
+
+subsection {* Generated Theorems
+  \label{ssec:codatatype-generated-theorems} *}
 
 
 section {* Defining Corecursive Functions
   \label{sec:defining-corecursive-functions} *}
 

 %%% 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} *}
+subsection {* Examples
+  \label{ssec:primcorec-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}).
-*}
-
-
-subsection {* General Syntax
-  \label{ssec:primcorec-general-syntax} *}
-
-
-subsection {* Characteristic Theorems
-  \label{ssec:primcorec-characteristic-theorems} *}
+codatatypes (Section~\ref{ssec:recursive-default-values-for-selectors}).
+*}
+
+
+subsection {* Syntax
+  \label{ssec:primcorec-syntax} *}
+
+text {*
+Primitive corecrusvie definitions have the following general syntax:
+
+@{rail "
+  @@{command primcorec} @{syntax target}? @{syntax \"fixes\"} \\ @'where'
+    (@{syntax primcorec_formula} + '|')
+  ;
+  @{syntax_def primcorec_formula}: @{syntax thmdecl}? @{syntax prop}
+    (@'of' (@{syntax term} * ))?
+"}
+*}
+
+
+subsection {* Generated Theorems
+  \label{ssec:primcorec-generated-theorems} *}
 
 
 section {* Registering Bounded Natural Functors
   \label{sec:registering-bounded-natural-functors} *}
 

     * @{command bnf}
     * @{command print_bnfs}
 *}
 
 
-subsection {* Introductory Example
-  \label{ssec:bnf-introductory-examples} *}
+subsection {* Example
+  \label{ssec:bnf-examples} *}
 
 text {*
 More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and
 \verb|~~/src/HOL/BNF/More_BNFs.thy|.
 
 Mention distinction between live and dead type arguments;
 mention =>.
 *}
 
 
-subsection {* General Syntax
-  \label{ssec:bnf-general-syntax} *}
+subsection {* Syntax
+  \label{ssec:bnf-syntax} *}
 
 
 section {* Generating Free Constructor Theorems
   \label{sec:generating-free-constructor-theorems} *}
 

   * @{command wrap_free_constructors}
     * \keyw{no\_dests}, \keyw{rep\_compat}
 *}
 
 
-subsection {* Introductory Example
-  \label{ssec:ctors-introductory-examples} *}
-
-
-subsection {* General Syntax
-  \label{ssec:ctors-general-syntax} *}
-
-
-subsection {* Characteristic Theorems
-  \label{ssec:ctors-characteristic-theorems} *}
+subsection {* Example
+  \label{ssec:ctors-examples} *}
+
+
+subsection {* Syntax
+  \label{ssec:ctors-syntax} *}
+
+
+subsection {* Generated Theorems
+  \label{ssec:ctors-generated-theorems} *}
 
 
 section {* Standard ML Interface
   \label{sec:standard-ml-interface} *}