--- a/src/Doc/Datatypes/Datatypes.thy Fri Sep 20 14:50:06 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Sep 20 15:05:47 2013 +0200
@@ -1410,7 +1410,7 @@
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")
codatatype 'a state_machine =
- State_Machine bool "'a \<Rightarrow> 'a state_machine"
+ State_Machine (accept: bool) (trans: "'a \<Rightarrow> 'a state_machine")
subsection {* Command Syntax
@@ -1764,6 +1764,30 @@
"of_dfa \<delta> F q = State_Machine (q \<in> F) (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:
+*}
+
+ primcorec empty_machine :: "'a state_machine" where
+ "empty_machine = State_Machine False (\<lambda>_. empty_machine)"
+ .
+
+ 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))"
+ .
+
+ primcorec_notyet plus_machine :: "'a state_machine \<Rightarrow> 'a state_machine" where
+ "or_machine M N =
+ State_Machine (accept M \<or> accept N)
+ (\<lambda>a. or_machine (trans M a) (trans N a))"
+
subsubsection {* Nested-as-Mutual Corecursion
\label{sssec:primcorec-nested-as-mutual-corecursion} *}