more (co)data docs

--- a/src/Doc/Datatypes/Datatypes.thy	Sun Sep 15 23:02:23 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Sun Sep 15 23:02:23 2013 +0200
@@ -9,9 +9,22 @@
 
 theory Datatypes
 imports Setup
+keywords
+  "primcorec_notyet" :: thy_decl
 begin
 
 
+(*<*)
+(* FIXME: Temporary setup until "primcorec" is fully implemented. *)
+ML_command {*
+fun add_dummy_cmd _ _ lthy = lthy;
+
+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} *}
 
@@ -28,7 +41,7 @@
 through a large class of non-datatypes, such as finite sets:
 *}
 
-    datatype_new 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s 'a "'a tree\<^sub>f\<^sub>s fset"
+    datatype_new 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s (lbl\<^sub>f\<^sub>s: 'a) (sub\<^sub>f\<^sub>s: "'a tree\<^sub>f\<^sub>s fset")
 
 text {*
 \noindent
@@ -63,10 +76,10 @@
 following four Rose tree examples:
 *}
 
-    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"
+    datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f (lbl\<^sub>f\<^sub>f: 'a) (sub\<^sub>f\<^sub>f: "'a tree\<^sub>f\<^sub>f list")
+    datatype_new 'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i (lbl\<^sub>f\<^sub>i: 'a) (sub\<^sub>f\<^sub>i: "'a tree\<^sub>f\<^sub>i llist")
+    codatatype 'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f (lbl\<^sub>i\<^sub>f: 'a) (sub\<^sub>i\<^sub>f: "'a tree\<^sub>i\<^sub>f list")
+    codatatype 'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i (lbl\<^sub>i\<^sub>i: 'a) (sub\<^sub>i\<^sub>i: "'a tree\<^sub>i\<^sub>i llist")
 (*<*)
     end
 (*>*)
@@ -166,9 +179,9 @@
 
 \begin{framed}
 \noindent
-\textbf{Warning:} This tutorial is under heavy construction. Please apologise
-for its appearance. If you have ideas regarding material that should be
-included, please let the authors know.
+\textbf{Warning:} This tutorial and the package it describes are under construction. Please apologise
+for their appearance. Should you have suggestions or comments regarding either,
+please let the authors know.
 \end{framed}
 *}
 
@@ -460,9 +473,9 @@
 should be generated.
 
 \item
-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
+The @{text "rep_compat"} option indicates that the generated names 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}
 
@@ -834,7 +847,6 @@
 *}
 
 
-(*
 subsection {* Compatibility Issues
   \label{ssec:datatype-compatibility-issues} *}
 
@@ -872,16 +884,17 @@
 %    * can also derive destructors etc. using @{command wrap_free_constructors}
 %      (Section XXX)
 *}
-*)
 
 
 section {* Defining Recursive Functions
   \label{sec:defining-recursive-functions} *}
 
 text {*
-This describes how to specify recursive functions over datatypes specified using
-@{command datatype_new}. The focus in on the @{command primrec_new} command,
-which supports primitive recursion. More examples can be found in
+Recursive functions over datatypes can be specified using @{command
+primrec_new}, which supports primitive recursion, or using the more general
+\keyw{fun} and \keyw{function} commands. Here, the focus is on @{command
+primrec_new}; the other two commands are described in a separate tutorial
+\cite{isabelle-function}. More examples can be found in the directory
 \verb|~~/src/HOL/BNF/Examples|.
 
 %%% TODO: partial_function
@@ -944,21 +957,21 @@
 (*>*)
     primrec_new replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
       "replicate Zero _ = []" |
-      "replicate (Suc n) a = a # replicate n a"
+      "replicate (Suc n) x = x # replicate n x"
 
 text {* \blankline *}
 
     primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
-      "at (a # as) j =
+      "at (x # xs) j =
          (case j of
-            Zero \<Rightarrow> a
-          | Suc j' \<Rightarrow> at as j')"
+            Zero \<Rightarrow> x
+          | Suc j' \<Rightarrow> at xs j')"
 
 text {* \blankline *}
 
     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)"
+      "tfold _ (TNil y) = y" |
+      "tfold f (TCons x xs) = f x (tfold f xs)"
 (*<*)
     end
 (*>*)
@@ -966,8 +979,8 @@
 text {*
 \noindent
 The next example is not primitive recursive, but it can be defined easily using
-@{command fun}. The @{command datatype_new_compat} command is needed to register
-new-style datatypes for use with @{command fun} and @{command function}
+\keyw{fun}. The @{command datatype_new_compat} command is needed to register
+new-style datatypes for use with \keyw{fun} and \keyw{function}
 (Section~\ref{sssec:datatype-new-compat}):
 *}
 
@@ -1011,7 +1024,7 @@
 
 text {*
 \noindent
-Mutual recursion is be possible within a single type, using @{command fun}:
+Mutual recursion is be possible within a single type, using \keyw{fun}:
 *}
 
     fun
@@ -1034,7 +1047,7 @@
 *}
 
 (*<*)
-    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>f = Node\<^sub>f\<^sub>f (lbl\<^sub>f\<^sub>f: 'a) (sub\<^sub>f\<^sub>f: "'a tree\<^sub>f\<^sub>f list")
 
     context dummy_tlist
     begin
@@ -1085,7 +1098,7 @@
 
 
 subsubsection {* Nested-as-Mutual Recursion
-  \label{sssec:datatype-nested-as-mutual-recursion} *}
+  \label{sssec:primrec-nested-as-mutual-recursion} *}
 
 text {*
 For compatibility with the old package, but also because it is sometimes
@@ -1301,7 +1314,7 @@
 be defined as a codatatype is that of the extended natural numbers:
 *}
 
-    codatatype enat = EZero | ESuc nat
+    codatatype enat = EZero | ESuc enat
 
 text {*
 \noindent
@@ -1331,8 +1344,8 @@
 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"
+    codatatype 'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i (lbl\<^sub>i\<^sub>i: 'a) (sub\<^sub>i\<^sub>i: "'a tree\<^sub>i\<^sub>i llist")
+    codatatype 'a tree\<^sub>i\<^sub>s = Node\<^sub>i\<^sub>s (lbl\<^sub>i\<^sub>s: 'a) (sub\<^sub>i\<^sub>s: "'a tree\<^sub>i\<^sub>s fset")
 
 
 subsection {* Command Syntax
@@ -1483,45 +1496,190 @@
 Whereas recursive functions consume datatypes one constructor at a time,
 corecursive functions construct codatatypes one constructor at a time.
 
+Corecursive functions over codatatypes can be specified using @{command
+primcorec}, which supports primitive corecursion, or using the more general
+\keyw{partial\_function} command. Here, the focus is on @{command primcorec}.
+More examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|.
+
 Reflecting a lack of agreement among proponents of coalgebraic methods, Isabelle
 supports two competing syntaxes for specifying a function $f$:
 
 \begin{itemize}
-\item Following the \emph{constructor view}, $f$ is specified by equations of
-the form
+\abovedisplayskip=.5\abovedisplayskip
+\belowdisplayskip=.5\belowdisplayskip
+
+\item The \emph{constructor view} specifies $f$ by equations of the form
 \[@{text "f x\<^sub>1 \<dots> x\<^sub>n = \<dots>"}\]
 Corecursive calls on
 the right-hand side must appear under a guarding codatatype constructor. Haskell
 and other lazy functional programming languages support this style.
 
-\item Following the \emph{destructor view}, $f$ is specified by implications
-of the form
+\item The \emph{destructor view} specifies $f$ by implications of the form
 \[@{text "\<dots> \<Longrightarrow> is_C\<^sub>j (f x\<^sub>1 \<dots> x\<^sub>n)"}\] and
 equations of the form
 \[@{text "un_C\<^sub>ji (f x\<^sub>1 \<dots> x\<^sub>n) = \<dots>"}\] where
 the right-hand side may be a corecursive call or an arbitrary term that does
-not mention @{text f}. This style is commonly found in the coalgebraic
-literature.
+not mention @{text f}. This style is favored in the coalgebraic literature.
 \end{itemize}
 
 \noindent
 Both styles are available as input syntax to @{command primcorec}. Whichever
-input syntax is chosen, characteristic theorems following both styles are
-generated.
+syntax is chosen, characteristic theorems following both styles are generated.
+
+\begin{framed}
+\noindent
+\textbf{Warning:} The @{command primcorec} command is under heavy development.
+Much of the functionality described here is vaporware. Until the command is
+fully in place, it is recommended to define corecursive functions directly using
+@{text unfold} or @{text corec}.
+\end{framed}
 
 %%% 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} *}
 
+
+subsubsection {* Simple Corecursion
+  \label{sssec:primcorec-simple-corecursion} *}
+
+    primcorec iterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
+      "iterate f x = LCons x (iterate f (f x))"
+    .
+
+(*<*)
+    locale dummy_dest_view
+    begin
+(*>*)
+    primcorec iterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
+      "\<not> lnull (iterate _ x)" |
+      "lhd (iterate _ x) = x" |
+      "ltl (iterate f x) = iterate f (f x)"
+    .
+(*<*)
+    end
+(*>*)
+
+    primcorec_notyet lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
+      "lappend xs ys =
+         (case xs of
+            LNil \<Rightarrow> ys
+          | LCons x xs' \<Rightarrow> LCons x (lappend xs' ys))"
+
+(*<*)
+    context dummy_dest_view
+    begin
+(*>*)
+    primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
+      "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lappend xs ys)" |
+      "lhd (lappend xs ys) =
+         (case xs of
+            LNil \<Rightarrow> lhd ys
+          | LCons x _ \<Rightarrow> x)" |
+      "ltl (lappend xs ys) =
+         (case xs of
+            LNil \<Rightarrow> ltl ys
+          | LCons _ xs \<Rightarrow> xs)"
+    .
+(*<*)
+    end
+(*>*)
+
+    primcorec infty :: enat where
+      "infty = ESuc infty"
+    .
+
+(*<*)
+    context dummy_dest_view
+    begin
+(*>*)
+    primcorec infty :: enat where
+      "\<not> is_EZero infty" |
+      "un_ESuc infty = infty"
+    .
+(*<*)
+    end
+(*>*)
+
+
+subsubsection {* Mutual Corecursion
+  \label{sssec:primcorec-mutual-corecursion} *}
+
+    primcorec
+      even_infty :: even_enat and
+      odd_infty :: odd_enat
+    where
+      "even_infty = Even_ESuc odd_infty" |
+      "odd_infty = Odd_ESuc even_infty"
+    .
+
+(*<*)
+    context dummy_dest_view
+    begin
+(*>*)
+    primcorec
+      even_infty :: even_enat and
+      odd_infty :: odd_enat
+    where
+      "\<not> is_Even_EZero even_infty" |
+      "un_Even_ESuc even_infty = odd_infty" |
+      "un_Odd_ESuc odd_infty = even_infty"
+    .
+(*<*)
+    end
+(*>*)
+
+
+subsubsection {* Nested Corecursion
+  \label{sssec:primcorec-nested-corecursion} *}
+
+    primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
+      "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i f) (f x))"
+    .
+
+    primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
+      "iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fmap (iterate\<^sub>i\<^sub>s f) (f x))"
+    .
+
 text {*
-More examples in \verb|~~/src/HOL/BNF/Examples|.
+Again, let us not forget our destructor-oriented passengers:
 *}
-*)
+
+(*<*)
+    context dummy_dest_view
+    begin
+(*>*)
+    primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
+      "lbl\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i f x) = x" |
+      "sub\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i f x) = lmap (iterate\<^sub>i\<^sub>i f) (f x)"
+    .
+(*<*)
+    end
+(*>*)
+
+
+subsubsection {* Nested-as-Mutual Corecursion
+  \label{sssec:primcorec-nested-as-mutual-corecursion} *}
+
+(*<*)
+    locale dummy_iterate
+    begin
+(*>*)
+    primcorec_notyet
+      iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" and
+      iterates\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a llist \<Rightarrow> 'a tree\<^sub>i\<^sub>i llist"
+    where
+      "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (iterates\<^sub>i\<^sub>i f (f x))" |
+      "iterates\<^sub>i\<^sub>i f xs =
+         (case xs of
+            LNil \<Rightarrow> LNil
+          | LCons x xs' \<Rightarrow> LCons (iterate\<^sub>i\<^sub>i f x) (iterates\<^sub>i\<^sub>i f xs'))"
+(*<*)
+    end
+(*>*)
 
 
 subsection {* Command Syntax