# HG changeset patch
# User blanchet
# Date 1380724181 -7200
# Node ID a3281fbe68568fb4485f07447aec113b4dedfa2a
# Parent  732b53d9b7206381c69038e15c4b9bb8315427fc
more (co)data docs

diff -r 732b53d9b720 -r a3281fbe6856 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Oct 02 16:29:40 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Oct 02 16:29:41 2013 +0200
@@ -1124,16 +1124,29 @@
 (@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
 *}
 
-    primrec_new ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
+    primrec_new (*<*)(in early) (*>*)ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
       "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
       "ftree_map f (FTNode g) = FTNode (ftree_map f \<circ> g)"
 
 text {*
 \noindent
-(No such function is defined by the package because @{typ 'a} is dead in
-@{typ "'a ftree"}, but we can easily do it ourselves.)
+(No such map function is defined by the package because the type
+variable @{typ 'a} is dead in @{typ "'a ftree"}.)
+
+Using \keyw{fun} or \keyw{function}, recursion through functions can be
+expressed using $\lambda$-expressions and function application rather
+than through composition. For example:
 *}
 
+    datatype_new_compat ftree
+
+text {* \blankline *}
+
+    function ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
+      "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
+      "ftree_map f (FTNode g) = FTNode (\<lambda>x. ftree_map f (g x))"
+    by auto (metis ftree.exhaust)
+
 
 subsubsection {* Nested-as-Mutual Recursion
   \label{sssec:primrec-nested-as-mutual-recursion} *}
@@ -1165,9 +1178,9 @@
 text {*
 \noindent
 Appropriate induction principles are generated under the names
-@{thm [source] "at\<^sub>f\<^sub>f.induct"},
-@{thm [source] "ats\<^sub>f\<^sub>f.induct"}, and
-@{thm [source] "at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct"}.
+@{thm [source] at\<^sub>f\<^sub>f.induct},
+@{thm [source] ats\<^sub>f\<^sub>f.induct}, and
+@{thm [source] at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct}.
 
 %%% TODO: Add recursors.
 
@@ -1514,7 +1527,7 @@
   \label{sssec:coinductive-theorems} *}
 
 text {*
-The coinductive theorems are as follows:
+The coinductive theorems are listed below for @{typ "'a llist"}:
 
 \begin{indentblock}
 \begin{description}
@@ -1539,11 +1552,11 @@
 Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be
 used to prove $m$ properties simultaneously.
 
-\item[@{text "t."}\hthm{unfold} \rm(@{text "[simp]"})\rm:] ~ \\
+\item[@{text "t."}\hthm{unfold}\rm:] ~ \\
 @{thm llist.unfold(1)[no_vars]} \\
 @{thm llist.unfold(2)[no_vars]}
 
-\item[@{text "t."}\hthm{corec} (@{text "[simp]"})\rm:] ~ \\
+\item[@{text "t."}\hthm{corec}\rm:] ~ \\
 @{thm llist.corec(1)[no_vars]} \\
 @{thm llist.corec(2)[no_vars]}
 
@@ -1580,9 +1593,9 @@
 \begin{indentblock}
 \begin{description}
 
-\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec}$^*$ @{text t.disc_corec}] ~ \\
-@{text t.disc_corec_iff} @{text t.sel_corec} @{text t.unfold}$^*$ @{text t.disc_unfold} @{text t.disc_unfold_iff} ~ \\
-@{text t.sel_unfold} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
+\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec} @{text t.disc_corec_iff}] ~ \\
+@{text t.sel_corec} @{text t.disc_unfold} @{text t.disc_unfold_iff} @{text t.sel_unfold} @{text t.map} \\
+@{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
 
 \end{description}
 \end{indentblock}
@@ -1780,7 +1793,7 @@
 
 text {*
 \noindent
-Deterministic finite automata (DFAs) are usually defined as 5-tuples
+Deterministic finite automata (DFAs) are traditionally 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}
 is an initial state, and @{text F} is a set of final states. The following
@@ -1796,8 +1809,8 @@
 \noindent
 The map function for the function type (@{text \<Rightarrow>}) is composition
 (@{text "op \<circ>"}). For convenience, corecursion through functions can be
-expressed using @{text \<lambda>}-expressions and function application rather
-than composition. For example:
+expressed using $\lambda$-expressions and function application rather
+than through composition. For example:
 *}
 
     primcorec