src/Doc/Datatypes/Datatypes.thy

 the following command introduces the type of lazy lists, which comprises both
 finite and infinite values:
 *}
 
 (*<*)
-    locale dummy_llist
-    begin
+    locale early
 (*>*)
-    codatatype 'a llist = LNil | LCons 'a "'a llist"
+    codatatype (*<*)(in early) (*>*)'a llist = LNil | LCons 'a "'a llist"
 
 text {*
 \noindent
 Mixed inductive--coinductive recursion is possible via nesting. Compare the
 following four Rose tree examples:
 *}
 
-    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
-(*>*)
+    datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
+    datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
+    codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
+    codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
 
 text {*
 The first two tree types allow only finite branches, whereas the last two allow
 branches of infinite length. Orthogonally, the nodes in the first and third
 types have finite branching, whereas those of the second and fourth may have

 text {*
 \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
-(*>*)
+    datatype_new (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
 
 text {*
 \noindent
 Occurrences of nonatomic types on the right-hand side of the equal sign must be
 enclosed in double quotes, as is customary in Isabelle.

       Cons (infixr "#" 65)
 
     hide_type list
     hide_const Nil Cons hd tl set map list_all2 list_case list_rec
 
-    locale dummy_list
-    begin
+    context early begin
 (*>*)
     datatype_new (set: 'a) list (map: map rel: list_all2) =
       null: Nil (defaults tl: Nil)
     | Cons (hd: 'a) (tl: "'a list")
 

 text {*
 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}
 \cite{isabelle-function}, Nitpick \cite{isabelle-nitpick}, Quickcheck,
 and other packages.
 
 \item It is extended by various add-ons, notably to produce instances of the

 
 text {*
 A few remarks concern nested recursive datatypes only:
 
 \begin{itemize}
+\setlength{\itemsep}{0pt}
+
 \item The old-style, nested-as-mutual induction rule, iterator theorems, and
 recursor theorems are generated under their usual names but with ``@{text
 "compat_"}'' prefixed (e.g., @{text compat_tree.induct}).
 
 \item All types through which recursion takes place must be new-style datatypes

 text {*
 The characteristic theorems generated by @{command datatype_new} are grouped in
 three broad categories:
 
 \begin{itemize}
+\setlength{\itemsep}{0pt}
+
 \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}.
 
 \item The \emph{functorial theorems} are properties of datatypes related to

 The command @{command datatype_new} was designed to be highly compatible with
 @{command datatype}, to ease migration. There are nonetheless a number of
 incompatibilities that may arise when porting to the new package:
 
 \begin{itemize}
+\setlength{\itemsep}{0pt}
+
 \item \emph{The Standard ML interfaces are different.} Tools and extensions
 written to call the old ML interfaces will need to be adapted to the new
 interfaces. Little has been done so far in this direction. Whenever possible, it
 is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype}
 to register new-style datatypes as old-style datatypes.

 text {*
 For simple recursive types, recursive calls on a constructor argument are
 allowed on the right-hand side:
 *}
 
-(*<*)
-    context dummy_tlist
-    begin
-(*>*)
     primrec_new replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
       "replicate Zero _ = []" |
       "replicate (Suc n) x = x # replicate n x"
 
 text {* \blankline *}

             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
+    primrec_new (*<*)(in early) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
       "tfold _ (TNil y) = y" |
       "tfold f (TCons x xs) = f x (tfold f xs)"
-(*<*)
-    end
-(*>*)
 
 text {*
 \noindent
 The next example is not primitive recursive, but it can be defined easily using
 \keyw{fun}. The @{command datatype_new_compat} command is needed to register

 recursive calls are lifted to lists using @{const map}:
 *}
 
 (*<*)
     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
 (*>*)
     primrec_new at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
       "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
          (case js of
             [] \<Rightarrow> a
           | j # js' \<Rightarrow> at (map (\<lambda>t. at\<^sub>f\<^sub>f t js') ts) j)"
-(*<*)
-    end
-(*>*)
 
 text {*
 \noindent
 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
 map function @{const option_map}:
 *}
 
-(*<*)
-    locale sum_btree_nested
-    begin
-(*>*)
-    primrec_new sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
+    primrec_new (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
       "sum_btree (BNode a lt rt) =
          a + the_default 0 (option_map sum_btree lt) +
            the_default 0 (option_map sum_btree rt)"
-(*<*)
-    end
-(*>*)
 
 text {*
 \noindent
 The same principle applies for arbitrary type constructors through which
 recursion is possible. Notably, the map function for the function type

 *}
 
 
 subsubsection {* Nested-as-Mutual Recursion
   \label{sssec:primrec-nested-as-mutual-recursion} *}
+
+(*<*)
+    locale n2m begin
+(*>*)
 
 text {*
 For compatibility with the old package, but also because it is sometimes
 convenient in its own right, it is possible to treat nested recursive datatypes
 as mutually recursive ones if the recursion takes place though new-style

 %     * the auxiliary functions like @{const ats\<^sub>f\<^sub>f} are sometimes useful in own right
 %
 %  * impact on automation unclear
 %
 *}
+(*<*)
+    end
+(*>*)
 
 
 subsection {* Command Syntax
   \label{ssec:primrec-command-syntax} *}
 

 text {*
 The characteristic theorems generated by @{command codatatype} are grouped in
 three broad categories:
 
 \begin{itemize}
+\setlength{\itemsep}{0pt}
+
 \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.

 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|.
 
-\begin{framed}
-\noindent
-\textbf{Warning:}\enskip 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 the generated @{text t_unfold} or @{text t_corec} combinators.
-\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} *}
-
-text {*
-Primitive corecursion is illustrated through concrete examples based on the
-codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
-examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|.
-*}
-
-
-subsubsection {* Simple Corecursion
-  \label{sssec:primcorec-simple-corecursion} *}
-
-text {*
 Whereas recursive functions consume datatypes one constructor at a time,
 corecursive functions construct codatatypes one constructor at a time.
 Reflecting a lack of agreement among proponents of coalgebraic methods, Isabelle
 supports two competing syntaxes for specifying a function $f$:
 
 \begin{itemize}
+\setlength{\itemsep}{0pt}
+
 \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>"}\]
-Lazy functional programming languages such as Haskell support this style.
 
 \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>"}\]
 This style is popular in the coalgebraic literature.
+
+\item The \emph{constructor view} specifies $f$ by equations of the form
+\[@{text "\<dots> \<Longrightarrow> f x\<^sub>1 \<dots> x\<^sub>n = C \<dots>"}\]
+
+\item The \emph{code view} specifies $f$ by a single equation of the form
+\[@{text "f x\<^sub>1 \<dots> x\<^sub>n = \<dots>"}\]
+with restrictions on the format of the right-hand side. Lazy functional
+programming languages such as Haskell support a generalized version of this
+style.
 \end{itemize}
 
 \noindent
-Both styles are available as input syntax to @{command primcorec}. Whichever
-syntax is chosen, characteristic theorems following both styles are generated.
-
-In the constructor view, corecursive calls are allowed on the right-hand side
-as long as they occur under a constructor. The constructor itself normally
-appears directly to the right of the equal sign:
+The constructor and code views coincide for functions that construct values
+using repeated applications of a single constructor.
+
+\noindent
+All three styles are available as input syntax to @{command primcorec}.
+Whichever syntax is chosen, characteristic theorems for all three styles are
+generated.
+
+\begin{framed}
+\noindent
+\textbf{Warning:}\enskip The @{command primcorec} command is under heavy
+development. Some of the functionality described here is vaporware. An
+alternative is to define corecursive functions directly using the generated
+@{text t_unfold} or @{text t_corec} combinators.
+\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} *}
+
+text {*
+Primitive corecursion is illustrated through concrete examples based on the
+codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
+examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|. The code
+view is favored in the examples below. Sections
+\ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view}
+present the same examples expressed using the constructor and destructor views.
+*}
+
+(*<*)
+    locale code_view
+    begin
+(*>*)
+
+subsubsection {* Simple Corecursion
+  \label{sssec:primcorec-simple-corecursion} *}
+
+text {*
+In the code view, corecursive calls are allowed on the right-hand side as long
+as they occur under a constructor, which itself appears either directly to the
+right of the equal sign or in a conditional expression:
 *}
 
     primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
       "literate f x = LCons x (literate f (f x))"
     .

     .
 
 text {*
 \noindent
 The constructor ensures that progress is made---i.e., the function is
-\emph{productive}. The above function computes the infinite lazy list or stream
+\emph{productive}. The above functions compute the infinite lazy list or stream
 @{text "[x, f x, f (f x), \<dots>]"}. Productivity guarantees that prefixes
 @{text "[x, f x, f (f x), \<dots>, (f ^^ k) x]"} of arbitrary finite length
-@{text k} can be computed by unfolding the equation a finite number of times.
-The period (\keyw{.}) at the end of the commands discharge the zero proof
+@{text k} can be computed by unfolding the code equation a finite number of
+times. The period (\keyw{.}) at the end of the commands discharge the zero proof
 obligations.
-
-These two functions can be specified as follows in the destructor view:
-*}
-
-(*<*)
-    locale dummy_dest_view
-    begin
-(*>*)
-    primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
-      "\<not> lnull (literate _ x)" |
-      "lhd (literate _ x) = x" |
-      "ltl (literate f x) = literate f (f x)"
-    .
-
-text {* \blankline *}
-
-    primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
-      "shd (siterate _ x) = x" |
-      "stl (siterate f x) = siterate f (f x)"
-    .
-(*<*)
-    end
-(*>*)
-
-text {*
-\noindent
-The first formula in the @{const literate} specification indicates which
-constructor to choose. For @{const siterate}, no such formula is necessary,
-since the type has only one constructor. The last two formulas are equations
-specifying the value of the result for the relevant selectors. Corecursive calls
-are allowed to appear directly to the right of the equal sign. Their arguments
-are unrestricted.
 
 Corecursive functions necessarily construct codatatype values. Nothing prevents
 them from also consuming such values. The following function drops ever second
 element in a stream:
 *}

     primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
       "every_snd s = SCons (shd s) (stl (stl s))"
     .
 
 text {*
-\noindent
-Here is the same example in the destructor view:
-*}
-
-(*<*)
-    context dummy_dest_view
-    begin
-(*>*)
-    primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
-      "shd (every_snd s) = shd s" |
-      "stl (every_snd s) = stl (stl s)"
-    .
-(*<*)
-    end
-(*>*)
-
-text {*
-In the constructor view, constructs such as @{text "let"}---@{text "in"}, @{text
+Constructs such as @{text "let"}---@{text "in"}, @{text
 "if"}---@{text "then"}---@{text "else"}, and @{text "case"}---@{text "of"} may
 appear around constructors that guard corecursive calls:
 *}
 
     primcorec_notyet lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where

          (case xs of
             LNil \<Rightarrow> ys
           | LCons x xs' \<Rightarrow> LCons x (lappend xs' ys))"
 
 text {*
-\noindent
-For this example, the destructor view is slighlty more involved, because it
-requires us to analyze the second argument (@{term 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) = lhd (if lnull xs then ys else xs)" |
-      "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
-    .
-(*<*)
-    end
-(*>*)
-
-text {*
 Corecursion is useful to specify not only functions but also infinite objects:
 *}
 
     primcorec infty :: enat where
       "infty = ESuc infty"
     .
-
-text {*
-\noindent
-Here is the example again for those passengers who prefer destructors:
-*}
-
-(*<*)
-    context dummy_dest_view
-    begin
-(*>*)
-    primcorec infty :: enat where
-      "\<not> is_EZero infty" |
-      "un_ESuc infty = infty"
-    .
-(*<*)
-    end
-(*>*)
 
 text {*
 The last example constructs a pseudorandom process value. It takes a stream of
 actions (@{text s}), a pseudorandom function generator (@{text f}), and a
 pseudorandom seed (@{text n}):

             Choice (random_process (every_snd s) (f \<circ> f) (f n))
               (random_process (every_snd (stl s)) (f \<circ> f) (f (f n))))"
 
 text {*
 \noindent
-The main disadvantage of the constructor view in this case is that the
-conditions are tested sequentially. This is visible in the generated theorems.
-In this respect, the destructor view is more elegant:
-*}
+The main disadvantage of the code view is that the conditions are tested
+sequentially. This is visible in the generated theorems. The constructor and
+destructor views offer non-sequential alternatives.
+*}
+
+
+subsubsection {* Mutual Corecursion
+  \label{sssec:primcorec-mutual-corecursion} *}
+
+text {*
+The syntax for mutually corecursive functions over mutually corecursive
+datatypes is unsurprising:
+*}
+
+    primcorec
+      even_infty :: even_enat and
+      odd_infty :: odd_enat
+    where
+      "even_infty = Even_ESuc odd_infty" |
+      "odd_infty = Odd_ESuc even_infty"
+    .
+
+
+subsubsection {* Nested Corecursion
+  \label{sssec:primcorec-nested-corecursion} *}
+
+text {*
+The next pair of examples generalize the @{const literate} and @{const siterate}
+functions (Section~\ref{sssec:primcorec-nested-corecursion}) to possibly
+infinite trees in which subnodes are organized either as a lazy list (@{text
+tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}):
+*}
+
+    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))"
+    .
+
+text {* \blankline *}
+
+    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 {*
+Deterministic finite automata (DFAs) are usually defined as 5-tuples
+@{text "(Q, \<Sigma>, \<delta>, q\<^sub>0, F)"}, where @{text Q} is a finite set of states,
+@{text \<Sigma>} is a finite alphabet, @{text \<delta>} is a transition function, @{text q\<^sub>0}
+is an initial state, and @{text F} is a set of final states. The following
+function translates a DFA into a @{type state_machine}:
+*}
+
+    primcorec of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine" where
+      "of_dfa \<delta> F q = State_Machine (q \<in> F) (of_dfa \<delta> F o \<delta> q)"
+    .
+
+
+subsubsection {* Nested-as-Mutual Corecursion
+  \label{sssec:primcorec-nested-as-mutual-corecursion} *}
+
+text {*
+Just as it is possible to recurse over nested recursive datatypes as if they
+were mutually recursive
+(Section~\ref{sssec:primrec-nested-as-mutual-recursion}), it is possible to
+corecurse over nested codatatypes as if they were mutually corecursive. For
+example:
+*}
+
+    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'))"
 
 (*<*)
-    context dummy_dest_view
+    end
+(*>*)
+
+
+subsubsection {* Constructor View
+  \label{ssec:primrec-constructor-view} *}
+
+(*<*)
+    locale ctr_view = code_view
     begin
 (*>*)
+
+text {*
+For the next example, the constructor view is slighlty more involved than the
+code equation:
+*}
+
+    primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
+      "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lappend xs ys = LNil" |
+      "_ \<Longrightarrow> lappend xs ys = LCons (lhd (if lnull xs then ys else xs))
+         (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
+    .
+
+text {*
+\noindent
+Recall the code view version presented in
+Section~\ref{sssec:primcorec-simple-corecursion}.
+% TODO: \[{thm code_view.lappend.code}\]
+The constructor view requires us to analyze the second argument (@{term ys}).
+The code equation generated for the constructor view also suffers from this
+complication.
+% TODO: \[{thm lappend.code}\]
+*}
+
+    primcorec_notyet random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" where
+      "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail" |
+      "n mod 4 = 1 \<Longrightarrow> random_process s f n = Skip (random_process s f (f n))" |
+      "n mod 4 = 2 \<Longrightarrow> random_process s f n =
+         Action (shd s) (random_process (stl s) f (f n))" |
+      "n mod 4 = 3 \<Longrightarrow> random_process s f n =
+         Choice (random_process (every_snd s) f (f n))
+           (random_process (every_snd (stl s)) f (f n))"
+    (* FIXME: by auto *)
+
+(*<*)
+    end
+(*>*)
+
+
+subsubsection {* Destructor View
+  \label{ssec:primrec-constructor-view} *}
+
+text {*
+The destructor view is in many respects dual to the constructor view. Conditions
+determine which constructor to choose, and these conditions are interpreted
+sequentially or not depending on the @{text "sequential"} option.
+
+Consider the following examples:
+*}
+
+(*<*)
+    locale dest_view
+    begin
+(*>*)
+
+    primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
+      "\<not> lnull (literate _ x)" |
+      "lhd (literate _ x) = x" |
+      "ltl (literate f x) = literate f (f x)"
+    .
+
+    primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
+      "shd (siterate _ x) = x" |
+      "stl (siterate f x) = siterate f (f x)"
+    .
+
+    primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
+      "shd (every_snd s) = shd s" |
+      "stl (every_snd s) = stl (stl s)"
+    .
+
+text {*
+\noindent
+The first formula in the @{const literate} specification indicates which
+constructor to choose. For @{const siterate} and @{const every_snd}, no such
+formula is necessary, since the type has only one constructor. The last two
+formulas are equations specifying the value of the result for the relevant
+selectors. Corecursive calls appear directly to the right of the equal sign.
+Their arguments are unrestricted.
+*}
+
     primcorec_notyet random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" where
       "n mod 4 = 0 \<Longrightarrow> is_Fail (random_process s f n)" |
       "n mod 4 = 1 \<Longrightarrow> is_Skip (random_process s f n)" |
       "n mod 4 = 2 \<Longrightarrow> is_Action (random_process s f n)" |
       "n mod 4 = 3 \<Longrightarrow> is_Choice (random_process s f n)" |
       "cont (random_process s f n) = random_process s f (f n)" (* of Skip FIXME *) |
       "prefix (random_process s f n) = shd s" |
       "cont (random_process s f n) = random_process (stl s) f (f n)" (* of Action FIXME *) |
       "left (random_process s f n) = random_process (every_snd s) f (f n)" |
       "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)"
-    (* by auto FIXME *)
-(*<*)
-    end
-(*>*)
-
-text {*
-\noindent
-The price to pay for this elegance is that we must discharge exclusivity proof
-obligations, one for each pair of conditions
-@{term "(n mod 4 = i, n mod 4 = j)"}. If we prefer not to discharge any
-obligations, we can specify the option @{text "(sequential)"} after the
-@{command primcorec} keyword. This pushes the problem to the users of the
-generated properties, as with the constructor view.
-*}
-
-
-subsubsection {* Mutual Corecursion
-  \label{sssec:primcorec-mutual-corecursion} *}
-
-text {*
-The syntax for mutually corecursive functions over mutually corecursive
-datatypes is anything but surprising. Following the constructor view:
-*}
-
-    primcorec
-      even_infty :: even_enat and
-      odd_infty :: odd_enat
-    where
-      "even_infty = Even_ESuc odd_infty" |
-      "odd_infty = Odd_ESuc even_infty"
-    .
-
-text {*
-And following the destructor view:
-*}
-
-(*<*)
-    context dummy_dest_view
-    begin
-(*>*)
+    (* FIXME: by auto *)
+
+text {*
+
+*}
+
     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} *}
-
-text {*
-The next pair of examples generalize the @{const literate} and @{const siterate}
-functions (Section~\ref{sssec:primcorec-nested-corecursion}) to possibly
-infinite trees in which subnodes are organized either as a lazy list (@{text
-tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}):
-*}
-
-    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))"
-    .
-
-text {* \blankline *}
-
-    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 {*
-Again, let us not forget our destructor-oriented passengers. Here is the first
-example in the destructor view:
-*}
-
-(*<*)
-    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
 (*>*)
 
-text {*
-Deterministic finite automata (DFAs) are usually defined as 5-tuples
-@{text "(Q, \<Sigma>, \<delta>, q\<^sub>0, F)"}, where @{text Q} is a finite set of states,
-@{text \<Sigma>} is a finite alphabet, @{text \<delta>} is a transition function, @{text q\<^sub>0}
-is an initial state, and @{text F} is a set of final states. The following
-function translates a DFA into a @{type state_machine}:
-*}
-
-    primcorec of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine" where
-      "of_dfa \<delta> F q = State_Machine (q \<in> F) (of_dfa \<delta> F o \<delta> q)"
-    .
-
-
-subsubsection {* Nested-as-Mutual Corecursion
-  \label{sssec:primcorec-nested-as-mutual-corecursion} *}
-
-text {*
-Just as it is possible to recurse over nested recursive datatypes as if they
-were mutually recursive
-(Section~\ref{sssec:primrec-nested-as-mutual-recursion}), it is possible to
-corecurse over nested codatatypes as if they were mutually corecursive. For
-example:
-*}
-
-(*<*)
-    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
   \label{ssec:primcorec-command-syntax} *}
 
 
 subsubsection {* \keyw{primcorec}

 
 text {*
 Primitive corecursive definitions have the following general syntax:
 
 @{rail "
-  @@{command_def primcorec} target? fixes \\ @'where'
-    (@{syntax primcorec_formula} + '|')
+  @@{command_def primcorec} target? @{syntax pcr_options}? fixes \\ @'where'
+    (@{syntax pcr_formula} + '|')
   ;
-  @{syntax_def primcorec_formula}: thmdecl? prop (@'of' (term * ))?
+  @{syntax_def pcr_options}: '(' 'sequential' ')'
+  ;
+  @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
 "}
+
+The optional target is optionally followed by a corecursion-specific option:
+
+\begin{itemize}
+\setlength{\itemsep}{0pt}
+
+\item
+The @{text "sequential"} option indicates that the conditions in specifications
+expressed using the constructor or destructor view are to be interpreted
+sequentially.
+\end{itemize}
+
 *}
 
 
 (*
 subsection {* Generated Theorems

 
 section {* Acknowledgments
   \label{sec:acknowledgments} *}
 
 text {*
-Tobias Nipkow and Makarius Wenzel have encouraged us to implement the new
+Tobias Nipkow and Makarius Wenzel encouraged us to implement the new
 (co)datatype package. Andreas Lochbihler provided lots of comments on earlier
 versions of the package, especially for the coinductive part. Brian Huffman
 suggested major simplifications to the internal constructions, much of which has
 yet to be implemented. Florian Haftmann and Christian Urban provided general
 advice on Isabelle and package writing. Stefan Milius and Lutz Schr\"oder