# HG changeset patch
# User blanchet
# Date 1378760977 -7200
# Node ID 2479b39d9d09ad2496fe04f932f5d4c044163056
# Parent  c413adedef469f88996675a5f5493da27a75f355
more docs

diff -r c413adedef46 -r 2479b39d9d09 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 09 20:24:15 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 09 23:09:37 2013 +0200
@@ -6,24 +6,8 @@
 
 theory Datatypes
 imports Setup
-keywords
-  "primrec_new_notyet" :: thy_decl and
-  "primcorec_notyet" :: thy_decl
 begin
 
-(*<*)
-(* FIXME: Evil setup until "primrec_new" and "primcorec" are bug-free. *)
-ML_command {*
-fun add_dummy_cmd _ _ lthy = lthy;
-
-val _ = Outer_Syntax.local_theory @{command_spec "primrec_new_notyet"} ""
-  (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd);
-
-val _ = Outer_Syntax.local_theory @{command_spec "primcorec_notyet"} ""
-  (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd);
-*}
-(*>*)
-
 
 section {* Introduction
   \label{sec:introduction} *}
@@ -182,6 +166,7 @@
 
 *}
 
+
 section {* Defining Datatypes
   \label{sec:defining-datatypes} *}
 
@@ -200,7 +185,7 @@
 
 text {*
 Datatypes are introduced by specifying the desired names and argument types for
-their constructors. \emph{Enumeration types} are the simplest form of datatype:
+their constructors. \emph{Enumeration} types are the simplest form of datatype.
 All their constructors are nullary:
 *}
 
@@ -208,7 +193,7 @@
 
 text {*
 \noindent
-All three constructors have the type @{typ trool}.
+Here, @{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}.
 
 Polymorphic types are possible, such as the following option type, modeled after
 its homologue from the @{theory Option} theory:
@@ -221,8 +206,8 @@
 
 text {*
 \noindent
-The constructors are @{term "None :: 'a option"} and
-@{term "Some :: 'a \<Rightarrow> 'a option"}.
+The constructors are @{text "None :: 'a option"} and
+@{text "Some :: 'a \<Rightarrow> 'a option"}.
 
 The next example has three type parameters:
 *}
@@ -232,7 +217,7 @@
 text {*
 \noindent
 The constructor is
-@{term "Triple :: 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a, 'b, 'c) triple"}.
+@{text "Triple :: 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a, 'b, 'c) triple"}.
 Unlike in Standard ML, curried constructors are supported. The uncurried variant
 is also possible:
 *}
@@ -243,7 +228,7 @@
 subsubsection {* Simple Recursion *}
 
 text {*
-simplest recursive type: copy of the natural numbers:
+Natural numbers are the simplest example of a recursive type:
 *}
 
     datatype_new nat = Zero | Suc nat
@@ -253,30 +238,41 @@
 (*>*)
 
 text {*
-lists were shown in the introduction; terminated lists are a variant:
+\noindent
+Lists were shown in the introduction. Terminated lists are a variant:
 *}
 
+(*<*)
+    locale dummy_tlist
+    begin
+(*>*)
     datatype_new ('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
+(*<*)
+    end
+(*>*)
 
 text {*
-On the right-hand side of the equal sign, the usual Isabelle conventions apply:
-Nonatomic types must be enclosed in double quotes.
+\noindent
+Nonatomic types must be enclosed in double quotes on the right-hand side of the
+equal sign, as is customary in Isabelle.
 *}
 
 
 subsubsection {* Mutual Recursion *}
 
 text {*
-Mutual recursion = Define several types simultaneously, referring to each other.
-
-Simple example: distinction between even and odd natural numbers:
+\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
 
 text {*
-More complex, and more realistic, example:
+\noindent
+Arithmetic expressions are defined via terms, terms via factors, and factors via
+expressions:
 *}
 
     datatype_new ('a, 'b) exp =
@@ -290,67 +286,81 @@
 subsubsection {* Nested Recursion *}
 
 text {*
-Nested recursion = Have recursion through a type constructor.
-
-The introduction showed some examples of trees with nesting through lists.
-
-More complex example, which reuses our option type:
+\emph{Nested recursion} occurs when recursive occurrences of a type appear under
+a type constructor. The introduction showed some examples of trees with nesting
+through lists. A more complex example, that reuses our @{text option} type,
+follows:
 *}
 
     datatype_new 'a btree =
       BNode 'a "'a btree option" "'a btree option"
 
 text {*
-Recursion may not be arbitrary; e.g. impossible to define
+\noindent
+Not all nestings are admissible. For example, this command will fail:
 *}
 
-    datatype_new 'a evil = Evil (*<*)'a
-    typ (*>*)"'a evil \<Rightarrow> 'a evil"
+    datatype_new 'a wrong = Wrong (*<*)'a
+    typ (*>*)"'a wrong \<Rightarrow> 'a wrong"
 
 text {*
-Issue: => allows recursion only on its right-hand side.
-This issue is inherited by polymorphic datatypes (and codatatypes)
-defined in terms of =>.
-In general, type constructors "('a1, ..., 'an) k" allow recursion on a subset
-of their type arguments.
+\noindent
+The issue is that the function arrow @{text "\<Rightarrow>"} allows recursion
+only through its right-hand side. This issue is inherited by polymorphic
+datatypes defined in terms of~@{text "\<Rightarrow>"}:
+*}
+
+    datatype_new ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
+    datatype_new 'a also_wrong = Also_Wrong (*<*)'a
+    typ (*>*)"('a also_wrong, 'a also_wrong) fn"
+
+text {*
+\noindent
+In general, type constructors @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
+allow recursion on a subset of their type arguments @{text 'a\<^sub>1}, \ldots,
+@{text 'a\<^sub>m}. These type arguments are called \emph{live}; the remaining
+type arguments are called \emph{dead}. In @{typ "'a \<Rightarrow> 'b"} and
+@{typ "('a, 'b) fn"}, the type variable @{typ 'a} is dead and @{typ 'b} is live.
 *}
 
 
 subsubsection {* Auxiliary Constants and Syntaxes *}
 
 text {*
-The @{command datatype_new} command introduces various constants in addition to the
-constructors. Given a type @{text "('a1,\<dots>,'aM) t"} with constructors
-@{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>m"}, the following auxiliary
-constants are introduced (among others):
+The @{command datatype_new} command introduces various constants in addition to
+the constructors. Given a type @{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 (among others):
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}
 
-\item \emph{Set functions} (\emph{natural transformations}):
-@{text t_set1}, \ldots, @{text t_setM}
+\item \relax{Set functions} (or \relax{natural transformations}):
+@{text t_set1}, \ldots, @{text t_setm}
 
-\item \emph{Map function} (\emph{functorial action}): @{text t_map}
+\item \relax{Map function} (or \relax{functorial action}): @{text t_map}
 
-\item \emph{Relator}: @{text t_rel}
+\item \relax{Relator}: @{text t_rel}
 
-\item \emph{Iterator}: @{text t_fold}
+\item \relax{Iterator}: @{text t_fold}
 
-\item \emph{Recursor}: @{text t_rec}
+\item \relax{Recursor}: @{text t_rec}
+
+\item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,
+@{text "t.is_C\<^sub>n"}
 
-\item \emph{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,
-@{text "t.is_C\<^sub>m"}
-
-\item \emph{Selectors}:
-@{text t.un_C}$_{11}$, \ldots, @{text t.un_C}$_{1n_1}$, \ldots,
-@{text t.un_C}$_{m1}$, \ldots, @{text t.un_C}$_{mn_m}$
+\item \relax{Selectors}:
+@{text t.un_C11}$, \ldots, @{text t.un_C1k\<^sub>1}, \\
+\phantom{\relax{Selectors:}} \quad\vdots \\
+\phantom{\relax{Selectors:}} @{text t.un_Cn1}$, \ldots, @{text t.un_Cnk\<^sub>n}.
 \end{itemize}
 
+\noindent
 The discriminators and selectors are collectively called \emph{destructors}. The
-@{text "t."} prefix is an optional component of the name and is normally hidden.
-
-The set functions, map function, relator, discriminators, and selectors can be
-given custom names, as in the example below:
+prefix ``@{text "t."}'' is an optional component of the name and is normally
+hidden. The set functions, map function, relator, discriminators, and selectors
+can be given custom names, as in the example below:
 *}
 
 (*<*)
@@ -380,26 +390,26 @@
   \qquad @{thm list.collapse(2)[of xs, no_vars]}\]
 %
 For two-constructor datatypes, a single discriminator constant suffices. The
-discriminator associated with @{const Cons} is simply @{text "\<not> null"}.
+discriminator associated with @{const Cons} is simply
+@{term "\<lambda>xs. \<not> null xs"}.
 
-The \keyw{defaults} keyword following the @{const Nil} constructor specifies a
-default value for selectors associated with other constructors. Here, it is
-used to specify that the tail of the empty list is the empty list (instead of
-being unspecified).
+The @{text "defaults"} keyword following the @{const Nil} constructor specifies
+a default value for selectors associated with other constructors. Here, it is
+used to ensure that the tail of the empty list is the empty list (instead of
+being left unspecified).
 
-Because @{const Nil} is a nullary constructor, it is also possible to use @{text
-"= Nil"} as a discriminator. This is specified by specifying @{text "="} instead
-of the identifier @{const null} in the declaration above. Although this may look
-appealing, the mixture of constructors and selectors in the resulting
-characteristic theorems can lead Isabelle's automation to switch between the
-constructor and the destructor view in surprising ways.
+Because @{const Nil} is a nullary constructor, it is also possible to use
+@{term "\<lambda>xs. xs = Nil"} as a discriminator. This is specified by
+entering ``@{text "="}'' instead of the identifier @{const null} in the
+declaration above. Although this may look appealing, the mixture of constructors
+and selectors in the resulting characteristic theorems can lead Isabelle's
+automation to switch between the constructor and the destructor view in
+surprising ways.
 *}
 
 text {*
-The usual mixfix syntaxes are available for both types and constructors. For example:
-
-%%% FIXME: remove trailing underscore and use locale trick instead once this is
-%%% supported.
+The usual mixfix syntaxes are available for both types and constructors. For
+example:
 *}
 
 (*<*)
@@ -645,9 +655,16 @@
             Zero \<Rightarrow> a
           | Suc j' \<Rightarrow> at as j')"
 
+(*<*)
+    context dummy_tlist
+    begin
+(*>*)
     primrec_new tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
       "tfold _ (TNil b) = b" |
       "tfold f (TCons a as) = f a (tfold f as)"
+(*<*)
+    end
+(*>*)
 
 text {*
 Show one example where fun is needed.
@@ -855,14 +872,14 @@
 
     consts termi\<^sub>0 :: 'a
 
-    datatype_new ('a, 'b) tlist_ =
+    datatype_new ('a, 'b) tlist =
       TNil (termi: 'b) (defaults ttl: TNil)
-    | TCons (thd: 'a) (ttl : "('a, 'b) tlist_") (defaults termi: "\<lambda>_ xs. termi\<^sub>0 xs")
+    | TCons (thd: 'a) (ttl : "('a, 'b) tlist") (defaults termi: "\<lambda>_ xs. termi\<^sub>0 xs")
 
     overloading
-      termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist_ \<Rightarrow> 'b"
+      termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist \<Rightarrow> 'b"
     begin
-    primrec_new termi\<^sub>0 :: "('a, 'b) tlist_ \<Rightarrow> 'b" where
+    primrec_new termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
     "termi\<^sub>0 (TNil y) = y" |
     "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
     end
diff -r c413adedef46 -r 2479b39d9d09 src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex	Mon Sep 09 20:24:15 2013 +0200
+++ b/src/Doc/Datatypes/document/root.tex	Mon Sep 09 23:09:37 2013 +0200
@@ -19,7 +19,9 @@
 
 \newcommand{\keyw}[1]{\isacommand{#1}}
 
-\renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$}
+%\renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$}
+\renewcommand{\isactrlsub}[1]{\/$\sb{#1}$}
+\renewcommand{\isadigit}[1]{\/\ensuremath{\mathrm{#1}}}
 \renewcommand{\isacharprime}{\isamath{{'}\mskip-2mu}}
 \renewcommand{\isacharunderscore}{\mbox{\_}}
 \renewcommand{\isacharunderscorekeyword}{\mbox{\_}}