src/Doc/Datatypes/Datatypes.thy

     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")
 
     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
   \label{ssec:codatatype-command-syntax} *}
 

 *}
 
     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)"
     .
+
+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} *}