# HG changeset patch
# User blanchet
# Date 1379681406 -7200
# Node ID 03c5c2db3a47e2ab6730607ca4a0b24a88a0364d
# Parent  b37db925b6635dee6b818cdb7f1b3ae86fce1f9c
more primcorec docs

diff -r b37db925b663 -r 03c5c2db3a47 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Sep 20 14:17:47 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Sep 20 14:50:06 2013 +0200
@@ -13,7 +13,6 @@
   "primcorec_notyet" :: thy_decl
 begin
 
-
 (*<*)
 (* FIXME: Temporary setup until "primcorec" is fully implemented. *)
 ML_command {*
@@ -1380,6 +1379,11 @@
     | Action (prefix: 'a) (cont: "'a process")
     | Choice (left: "'a process") (right: "'a process")
 
+text {*
+Notice that the @{const cont} selector is associated with both @{const Skip}
+and @{const Choice}.
+*}
+
 
 subsubsection {* Mutual Corecursion
   \label{sssec:codatatype-mutual-corecursion} *}
@@ -1796,8 +1800,12 @@
 (*>*)
 
 text {*
-For the next example, the constructor view is slighlty more involved than the
-code equation:
+The constructor view is similar to the code view, but there is one separate
+conditional equation per constructor rather than a single unconditional
+equation. Examples that rely on a single constructor, such as @{const literate}
+and @{const siterate}, are identical in both styles.
+
+Here is an example where there is a difference:
 *}
 
     primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
@@ -1808,13 +1816,20 @@
 
 text {*
 \noindent
-Recall the code view version presented in
+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.
+
+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.
 % TODO: \[{thm lappend.code}\]
+
+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
@@ -1831,6 +1846,20 @@
     end
 (*>*)
 
+text {*
+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"}.
+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.
+
+%Here are more examples to conclude:
+*}
+
 
 subsubsection {* Destructor View
   \label{ssec:primrec-constructor-view} *}
@@ -1872,6 +1901,46 @@
 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.
+
+The next example shows how to specify functions that rely on more than one
+constructor:
+*}
+
+    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)"
+    .
+
+text {*
+\noindent
+For a codatatype with $n$ constructors, it is sufficient to specify $n - 1$
+discriminator formulas. The command will then assume that the remaining
+constructor should be taken otherwise. This can be made explicit by adding
+*}
+
+(*<*)
+    end
+
+    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)" (*<*) |
+      "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)"
+    .
+
+    context dest_view begin
+(*>*)
+
+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
+constructors:
 *}
 
     primcorec_notyet random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" where
@@ -1887,7 +1956,11 @@
     (* FIXME: by auto *)
 
 text {*
-
+\noindent
+Using the @{text "of"} keyword, different equations are specified for @{const
+cont} depending on which constructor is selected.
+
+Here are more examples to conclude:
 *}
 
     primcorec
@@ -1908,6 +1981,7 @@
     end
 (*>*)
 
+
 subsection {* Command Syntax
   \label{ssec:primcorec-command-syntax} *}
 
@@ -2147,5 +2221,4 @@
 suggested an elegant proof to eliminate one of the BNF assumptions.
 *}
 
-
 end