# HG changeset patch
# User blanchet
# Date 1379684561 -7200
# Node ID 1a883094fbe02ecec6cf94b9e64f9492208ec9fc
# Parent  7a994dc08cea8e2379fdfcafef6eeeaf89672cb3
more primcorec docs

diff -r 7a994dc08cea -r 1a883094fbe0 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Sep 20 15:05:47 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Sep 20 15:42:41 2013 +0200
@@ -122,7 +122,7 @@
 @{command primrec_new}, \keyw{fun}, and \keyw{function}.
 
 \item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
-describes how to specify codatatypes using the @{command codatatype} command.
+describes how to specify codatatypes using the \keyw{codatatype} command.
 
 \item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive
 Functions,'' describes how to specify corecursive functions using the
@@ -137,7 +137,7 @@
 ``Deriving Destructors and Theorems for Free Constructors,'' explains how to
 use the command @{command wrap_free_constructors} to derive destructor constants
 and theorems for freely generated types, as performed internally by @{command
-datatype_new} and @{command codatatype}.
+datatype_new} and \keyw{codatatype}.
 
 %\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
 %describes the package's programmatic interface.
@@ -341,7 +341,7 @@
 
 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.
+datatype_new} and \keyw{codatatype} commands.
 Section~\ref{sec:registering-bounded-natural-functors} explains how to register
 arbitrary type constructors as BNFs.
 *}
@@ -864,7 +864,7 @@
 
 text {*
 The command @{command datatype_new} was designed to be highly compatible with
-@{command datatype}, to ease migration. There are nonetheless a number of
+\keyw{datatype}, to ease migration. There are nonetheless a number of
 incompatibilities that may arise when porting to the new package:
 
 \begin{itemize}
@@ -1044,6 +1044,8 @@
       "nat_of_even_nat (Even_Suc n) = Suc (nat_of_odd_nat n)" |
       "nat_of_odd_nat (Odd_Suc n) = Suc (nat_of_even_nat n)"
 
+text {* \blankline *}
+
     primrec_new
       eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
       eval\<^sub>t :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) trm \<Rightarrow> int" and
@@ -1320,7 +1322,7 @@
   \label{sec:defining-codatatypes} *}
 
 text {*
-Codatatypes can be specified using the @{command codatatype} command. The
+Codatatypes can be specified using the \keyw{codatatype} command. The
 command is first illustrated through concrete examples featuring different
 flavors of corecursion. More examples can be found in the directory
 \verb|~~/src/HOL/BNF/Examples|. The \emph{Archive of Formal Proofs} also
@@ -1407,8 +1409,12 @@
 
     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")
 
+text {* \blankline *}
+
     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")
 
+text {* \blankline *}
+
     codatatype 'a state_machine =
       State_Machine (accept: bool) (trans: "'a \<Rightarrow> 'a state_machine")
 
@@ -1423,7 +1429,7 @@
 text {*
 Definitions of codatatypes have almost exactly the same syntax as for datatypes
 (Section~\ref{ssec:datatype-command-syntax}), with two exceptions: The command
-is called @{command codatatype}. The @{text "no_discs_sels"} option is not
+is called \keyw{codatatype}. The @{text "no_discs_sels"} option is not
 available, because destructors are a crucial notion for codatatypes.
 *}
 
@@ -1453,7 +1459,7 @@
   \label{ssec:codatatype-generated-theorems} *}
 
 text {*
-The characteristic theorems generated by @{command codatatype} are grouped in
+The characteristic theorems generated by \keyw{codatatype} are grouped in
 three broad categories:
 
 \begin{itemize}
@@ -1541,7 +1547,7 @@
 \end{indentblock}
 
 \noindent
-For convenience, @{command codatatype} also provides the following collection:
+For convenience, \keyw{codatatype} also provides the following collection:
 
 \begin{indentblock}
 \begin{description}
@@ -1559,16 +1565,15 @@
   \label{sec:defining-corecursive-functions} *}
 
 text {*
-Corecursive functions can be specified using the @{command primcorec} command.
-Corecursive functions over codatatypes can be specified using @{command
-primcorec}, which supports primitive corecursion, or using the more general
+Corecursive functions 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|.
 
 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$:
+Partly reflecting a lack of agreement among proponents of coalgebraic methods,
+Isabelle supports three competing syntaxes for specifying a function $f$:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}
@@ -1584,6 +1589,7 @@
 
 \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>"}\]
+This style is often more concise than the previous one.
 
 \item The \emph{code view} specifies $f$ by a single equation of the form
 \[@{text "f x\<^sub>1 \<dots> x\<^sub>n = \<dots>"}\]
@@ -1592,21 +1598,16 @@
 style.
 \end{itemize}
 
-\noindent
-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.
+\textbf{Warning:}\enskip The @{command primcorec} command is under 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
@@ -1635,9 +1636,9 @@
   \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:
+Following 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
@@ -1660,8 +1661,8 @@
 times. The period (\keyw{.}) at the end of the commands discharge the zero proof
 obligations.
 
-Corecursive functions necessarily construct codatatype values. Nothing prevents
-them from also consuming such values. The following function drops ever second
+Corecursive functions construct codatatype values, but nothing prevents them
+from also consuming such values. The following function drops ever second
 element in a stream:
 *}
 
@@ -1670,6 +1671,7 @@
     .
 
 text {*
+\noindent
 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:
@@ -1682,6 +1684,7 @@
           | LCons x xs' \<Rightarrow> LCons x (lappend xs' ys))"
 
 text {*
+\noindent
 Corecursion is useful to specify not only functions but also infinite objects:
 *}
 
@@ -1690,12 +1693,15 @@
     .
 
 text {*
-The last example constructs a pseudorandom process value. It takes a stream of
+\noindent
+The example below 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}):
 *}
 
-    primcorec_notyet random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" where
+    primcorec_notyet
+      random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
+    where
       "random_process s f n =
          (if n mod 4 = 0 then
             Fail
@@ -1711,7 +1717,7 @@
 \noindent
 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.
+destructor views offer nonsequential alternatives.
 *}
 
 
@@ -1753,6 +1759,7 @@
     .
 
 text {*
+\noindent
 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}
@@ -1760,33 +1767,47 @@
 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)"
+    primcorec (*<*)(in early) (*>*)
+      sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
+    where
+      "sm_of_dfa \<delta> F q = State_Machine (q \<in> F) (sm_of_dfa \<delta> F o \<delta> q)"
     .
 
 text {*
 \noindent
 The map function for the function type (@{text \<Rightarrow>}) is composition
-(@{text "op \<circ>"}).
-
-\noindent
-For convenience, corecursion through functions can be expressed using
-@{text \<lambda>}-expressions and function application rather than composition.
-For example:
+(@{text "op \<circ>"}). For convenience, corecursion through functions can be
+expressed using @{text \<lambda>}-expressions and function application rather
+than composition. For example:
 *}
 
-    primcorec empty_machine :: "'a state_machine" where
-      "empty_machine = State_Machine False (\<lambda>_. empty_machine)"
+    primcorec
+      sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
+    where
+      "sm_of_dfa \<delta> F q = State_Machine (q \<in> F) (sm_of_dfa \<delta> F o \<delta> q)"
+    .
+
+text {* \blankline *}
+
+    primcorec empty_sm :: "'a state_machine" where
+      "empty_sm = State_Machine False (\<lambda>_. empty_sm)"
     .
 
-    primcorec not_machine :: "'a state_machine \<Rightarrow> 'a state_machine" where
-      "not_machine M = State_Machine (\<not> accept M) (\<lambda>a. not_machine (trans M a))"
+text {* \blankline *}
+
+    primcorec not_sm :: "'a state_machine \<Rightarrow> 'a state_machine" where
+      "not_sm M = State_Machine (\<not> accept M) (\<lambda>a. not_sm (trans M a))"
     .
 
-    primcorec_notyet plus_machine :: "'a state_machine \<Rightarrow> 'a state_machine" where
-      "or_machine M N =
+text {* \blankline *}
+
+    primcorec
+      or_sm :: "'a state_machine \<Rightarrow> 'a state_machine \<Rightarrow> 'a state_machine"
+    where
+      "or_sm M N =
          State_Machine (accept M \<or> accept N)
-           (\<lambda>a. or_machine (trans M a) (trans N a))"
+           (\<lambda>a. or_sm (trans M a) (trans N a))"
+    .
 
 
 subsubsection {* Nested-as-Mutual Corecursion
@@ -1796,8 +1817,7 @@
 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:
+pretend that nested codatatypes are mutually corecursive. For example:
 *}
 
     primcorec_notyet
@@ -1840,78 +1860,83 @@
 
 text {*
 \noindent
-With the constructor view, we must now distinguish between the @{const LNil}
-case and the @{const LCons} case. The condition for the @{const LCons} case is
-left implicit, as the negation of the @{const LNil} case.
+With the constructor view, we must distinguish between the @{const LNil} and
+the @{const LCons} case. The condition for @{const LCons} is
+left implicit, as the negation of that for @{const LNil}.
 
 For this example, the constructor view is slighlty more involved than the
 code equation. 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.
+The code equation generated from the constructor view also suffers from this.
 % TODO: \[{thm lappend.code}\]
 
-The next example is arguably more naturally expressed in the constructor view:
+In contrast, the next example is arguably more naturally expressed in the
+constructor view:
 *}
 
-    primcorec_notyet random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" where
+    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))"
+      "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
 (*>*)
 
 text {*
+\noindent
 Since there is no sequentiality, we can apply the equation for @{const Choice}
-without having first to discharge @{term "n mod 4 \<noteq> 0"},
-@{term "n mod 4 \<noteq> 1"}, and @{term "n mod 4 \<noteq> 2"}.
+without having first to discharge @{term "n mod (4\<Colon>int) \<noteq> 0"},
+@{term "n mod (4\<Colon>int) \<noteq> 1"}, and
+@{term "n mod (4\<Colon>int) \<noteq> 2"}.
 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 code view.
-
+@{term "(n mod (4\<Colon>int) = i, n mod (4\<Colon>int) = j)"}
+with @{term "i < j"}. If we prefer not to discharge any obligations, we can
+enable the @{text "sequential"} option. This pushes the problem to the users of
+the generated properties.
 %Here are more examples to conclude:
 *}
 
 
 subsubsection {* Destructor View
-  \label{ssec:primrec-constructor-view} *}
+  \label{ssec:primrec-destructor-view} *}
+
+(*<*)
+    locale dest_view
+    begin
+(*>*)
 
 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)"
     .
 
+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)"
     .
 
+text {* \blankline *}
+
     primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
       "shd (every_snd s) = shd s" |
       "stl (every_snd s) = stl (stl s)"
@@ -1949,7 +1974,8 @@
     primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
       "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lappend xs ys)" |
 (*>*)
-      "_ \<Longrightarrow> \<not> lnull (lappend xs ys)" (*<*) |
+      "_ \<Longrightarrow> \<not> 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)"
     .
@@ -1959,15 +1985,15 @@
 
 text {*
 \noindent
-to the specification.
-In the generated theorems, the selector equations are conditional:
-\[@{thm lappend.sel}\]
-
-The next example shows how to cope with selectors defined for several
+to the specification. The generated selector theorems are conditional.
+
+The next example illustrates how to cope with selectors defined for several
 constructors:
 *}
 
-    primcorec_notyet random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" where
+    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)" |
@@ -1976,8 +2002,9 @@
       "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)"
+      "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)" (*<*)
     (* FIXME: by auto *)
+(*>*)
 
 text {*
 \noindent
@@ -1996,6 +2023,8 @@
       "un_Odd_ESuc odd_infty = even_infty"
     .
 
+text {* \blankline *}
+
     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)"
@@ -2112,7 +2141,7 @@
 
 text {*
 The derivation of convenience theorems for types equipped with free constructors,
-as performed internally by @{command datatype_new} and @{command codatatype},
+as performed internally by @{command datatype_new} and \keyw{codatatype},
 is available as a stand-alone command called @{command wrap_free_constructors}.
 
 %  * need for this is rare but may arise if you want e.g. to add destructors to