1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Oct 02 16:29:40 2013 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Oct 02 16:29:41 2013 +0200
     1.3 @@ -1124,16 +1124,29 @@
     1.4  (@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
     1.5  *}
     1.6  
     1.7 -    primrec_new ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
     1.8 +    primrec_new (*<*)(in early) (*>*)ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
     1.9        "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
    1.10        "ftree_map f (FTNode g) = FTNode (ftree_map f \<circ> g)"
    1.11  
    1.12  text {*
    1.13  \noindent
    1.14 -(No such function is defined by the package because @{typ 'a} is dead in
    1.15 -@{typ "'a ftree"}, but we can easily do it ourselves.)
    1.16 +(No such map function is defined by the package because the type
    1.17 +variable @{typ 'a} is dead in @{typ "'a ftree"}.)
    1.18 +
    1.19 +Using \keyw{fun} or \keyw{function}, recursion through functions can be
    1.20 +expressed using $\lambda$-expressions and function application rather
    1.21 +than through composition. For example:
    1.22  *}
    1.23  
    1.24 +    datatype_new_compat ftree
    1.25 +
    1.26 +text {* \blankline *}
    1.27 +
    1.28 +    function ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
    1.29 +      "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
    1.30 +      "ftree_map f (FTNode g) = FTNode (\<lambda>x. ftree_map f (g x))"
    1.31 +    by auto (metis ftree.exhaust)
    1.32 +
    1.33  
    1.34  subsubsection {* Nested-as-Mutual Recursion
    1.35    \label{sssec:primrec-nested-as-mutual-recursion} *}
    1.36 @@ -1165,9 +1178,9 @@
    1.37  text {*
    1.38  \noindent
    1.39  Appropriate induction principles are generated under the names
    1.40 -@{thm [source] "at\<^sub>f\<^sub>f.induct"},
    1.41 -@{thm [source] "ats\<^sub>f\<^sub>f.induct"}, and
    1.42 -@{thm [source] "at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct"}.
    1.43 +@{thm [source] at\<^sub>f\<^sub>f.induct},
    1.44 +@{thm [source] ats\<^sub>f\<^sub>f.induct}, and
    1.45 +@{thm [source] at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct}.
    1.46  
    1.47  %%% TODO: Add recursors.
    1.48  
    1.49 @@ -1514,7 +1527,7 @@
    1.50    \label{sssec:coinductive-theorems} *}
    1.51  
    1.52  text {*
    1.53 -The coinductive theorems are as follows:
    1.54 +The coinductive theorems are listed below for @{typ "'a llist"}:
    1.55  
    1.56  \begin{indentblock}
    1.57  \begin{description}
    1.58 @@ -1539,11 +1552,11 @@
    1.59  Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be
    1.60  used to prove $m$ properties simultaneously.
    1.61  
    1.62 -\item[@{text "t."}\hthm{unfold} \rm(@{text "[simp]"})\rm:] ~ \\
    1.63 +\item[@{text "t."}\hthm{unfold}\rm:] ~ \\
    1.64  @{thm llist.unfold(1)[no_vars]} \\
    1.65  @{thm llist.unfold(2)[no_vars]}
    1.66  
    1.67 -\item[@{text "t."}\hthm{corec} (@{text "[simp]"})\rm:] ~ \\
    1.68 +\item[@{text "t."}\hthm{corec}\rm:] ~ \\
    1.69  @{thm llist.corec(1)[no_vars]} \\
    1.70  @{thm llist.corec(2)[no_vars]}
    1.71  
    1.72 @@ -1580,9 +1593,9 @@
    1.73  \begin{indentblock}
    1.74  \begin{description}
    1.75  
    1.76 -\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec}$^*$ @{text t.disc_corec}] ~ \\
    1.77 -@{text t.disc_corec_iff} @{text t.sel_corec} @{text t.unfold}$^*$ @{text t.disc_unfold} @{text t.disc_unfold_iff} ~ \\
    1.78 -@{text t.sel_unfold} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
    1.79 +\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec} @{text t.disc_corec_iff}] ~ \\
    1.80 +@{text t.sel_corec} @{text t.disc_unfold} @{text t.disc_unfold_iff} @{text t.sel_unfold} @{text t.map} \\
    1.81 +@{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
    1.82  
    1.83  \end{description}
    1.84  \end{indentblock}
    1.85 @@ -1780,7 +1793,7 @@
    1.86  
    1.87  text {*
    1.88  \noindent
    1.89 -Deterministic finite automata (DFAs) are usually defined as 5-tuples
    1.90 +Deterministic finite automata (DFAs) are traditionally defined as 5-tuples
    1.91  @{text "(Q, \<Sigma>, \<delta>, q\<^sub>0, F)"}, where @{text Q} is a finite set of states,
    1.92  @{text \<Sigma>} is a finite alphabet, @{text \<delta>} is a transition function, @{text q\<^sub>0}
    1.93  is an initial state, and @{text F} is a set of final states. The following
    1.94 @@ -1796,8 +1809,8 @@
    1.95  \noindent
    1.96  The map function for the function type (@{text \<Rightarrow>}) is composition
    1.97  (@{text "op \<circ>"}). For convenience, corecursion through functions can be
    1.98 -expressed using @{text \<lambda>}-expressions and function application rather
    1.99 -than composition. For example:
   1.100 +expressed using $\lambda$-expressions and function application rather
   1.101 +than through composition. For example:
   1.102  *}
   1.103  
   1.104      primcorec