src/Doc/Datatypes/Datatypes.thy

 
 Tutorial for (co)datatype definitions with the new package.
 *)
 
 theory Datatypes
-imports Setup
+imports Setup "~~/src/HOL/Library/Simps_Case_Conv"
 begin
 
 section {* Introduction
   \label{sec:introduction} *}
 

       "tfold _ (TNil y) = y" |
       "tfold f (TCons x xs) = f x (tfold f xs)"
 
 text {*
 \noindent
+Pattern matching is only available for the argument on which the recursion takes
+place. Fortunately, it is easy to generate pattern-maching equations using the
+\keyw{simps\_of\_case} command provided by the theory
+\verb|~~/src/HOL/Library/Simps_Case_Conv|.
+*}
+
+    simps_of_case at_simps: at.simps
+
+text {*
+This generates the lemma collection @{thm [source] at_simps}:
+%
+\[@{thm at_simps(1)[no_vars]}
+  \qquad @{thm at_simps(2)[no_vars]}\]
+%
 The next example is defined using \keyw{fun} to escape the syntactic
 restrictions imposed on primitive recursive functions. The
 @{command datatype_new_compat} command is needed to register new-style datatypes
 for use with \keyw{fun} and \keyw{function}
 (Section~\ref{sssec:datatype-new-compat}):

             LNil \<Rightarrow> ys
           | LCons x xs' \<Rightarrow> LCons x (lappend xs' ys))"
 
 text {*
 \noindent
+Pattern matching is not supported by @{command primcorec}. Fortunately, it is
+easy to generate pattern-maching equations using the \keyw{simps\_of\_case}
+command provided by the theory \verb|~~/src/HOL/Library/Simps_Case_Conv|.
+*}
+
+    simps_of_case lappend_simps: lappend.code
+
+text {*
+This generates the lemma collection @{thm [source] lappend_simps}:
+%
+\[@{thm lappend_simps(1)[no_vars]}
+  \qquad @{thm lappend_simps(2)[no_vars]}\]
+%
 Corecursion is useful to specify not only functions but also infinite objects:
 *}
 
     primcorec infty :: enat where
       "infty = ESuc infty"