# HG changeset patch
# User blanchet
# Date 1384260444 -3600
# Node ID 5d1b7ee6070e958a0bd538c3ec0833377d58d57c
# Parent  f6950854855d3675566f7c4ebb7caff11287044f
document idiomatic use of 'simps_of_case'

diff -r f6950854855d -r 5d1b7ee6070e src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Nov 12 13:47:24 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Nov 12 13:47:24 2013 +0100
@@ -8,7 +8,7 @@
 *)
 
 theory Datatypes
-imports Setup
+imports Setup "~~/src/HOL/Library/Simps_Case_Conv"
 begin
 
 section {* Introduction
@@ -1052,6 +1052,20 @@
 
 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
@@ -1759,6 +1773,19 @@
 
 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:
 *}