--- a/src/Doc/Datatypes/Datatypes.thy Fri Sep 20 12:09:06 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Sep 20 14:17:47 2013 +0200
@@ -65,10 +65,9 @@
*}
(*<*)
- 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
@@ -76,13 +75,10 @@
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
@@ -262,14 +258,7 @@
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
@@ -384,8 +373,7 @@
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)
@@ -551,6 +539,8 @@
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.
@@ -586,6 +576,8 @@
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}).
@@ -653,6 +645,8 @@
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}.
@@ -875,6 +869,8 @@
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
@@ -998,10 +994,6 @@
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"
@@ -1016,12 +1008,9 @@
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
@@ -1095,18 +1084,12 @@
(*<*)
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
@@ -1115,17 +1098,10 @@
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
@@ -1148,6 +1124,10 @@
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
@@ -1217,6 +1197,9 @@
% * impact on automation unclear
%
*}
+(*<*)
+ end
+(*>*)
subsection {* Command Syntax
@@ -1470,6 +1453,8 @@
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.
@@ -1576,12 +1561,48 @@
\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$:
+
+\begin{itemize}
+\setlength{\itemsep}{0pt}
+
+\abovedisplayskip=.5\abovedisplayskip
+\belowdisplayskip=.5\belowdisplayskip
+
+\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
+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. 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.
+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
@@ -1595,41 +1616,24 @@
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|.
+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 {*
-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}
-\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.
-\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:
+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
@@ -1645,45 +1649,13 @@
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:
@@ -1694,24 +1666,7 @@
.
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:
*}
@@ -1723,25 +1678,6 @@
| 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:
*}
@@ -1750,23 +1686,6 @@
.
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}):
@@ -1786,38 +1705,9 @@
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:
-*}
-
-(*<*)
- context dummy_dest_view
- begin
-(*>*)
- 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.
+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.
*}
@@ -1826,7 +1716,7 @@
text {*
The syntax for mutually corecursive functions over mutually corecursive
-datatypes is anything but surprising. Following the constructor view:
+datatypes is unsurprising:
*}
primcorec
@@ -1837,26 +1727,6 @@
"odd_infty = Odd_ESuc even_infty"
.
-text {*
-And following the destructor view:
-*}
-
-(*<*)
- 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} *}
@@ -1879,23 +1749,6 @@
.
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}
@@ -1919,10 +1772,6 @@
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"
@@ -1932,11 +1781,133 @@
(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
+(*>*)
+
+
+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)"
+ (* 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"
+ .
+
+ 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
+(*>*)
+
subsection {* Command Syntax
\label{ssec:primcorec-command-syntax} *}
@@ -1948,11 +1919,25 @@
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 pcr_options}: '(' 'sequential' ')'
;
- @{syntax_def primcorec_formula}: thmdecl? prop (@'of' (term * ))?
+ @{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}
+
*}
@@ -2153,7 +2138,7 @@
\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