# HG changeset patch
# User blanchet
# Date 1449261578 -3600
# Node ID 0ccb1eaa2184a10909df0b5ab8e0969efe374cba
# Parent  6c42d55097c1b428c42d731aa1d06866ff54a757
more documentation on 'size' plugin

diff -r 6c42d55097c1 -r 0ccb1eaa2184 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Dec 04 21:21:35 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Dec 04 21:39:38 2015 +0100
@@ -3178,11 +3178,11 @@
   \label{ssec:size} *}
 
 text {*
-For each datatype, the \hthm{size} plugin generates a generic size
+For each datatype @{text t}, the \hthm{size} plugin generates a generic size
 function @{text "t.size_t"} as well as a specific instance
-@{text "size :: t \<Rightarrow> nat"} belonging to the @{text size} type
-class. The \keyw{fun} command relies on @{const size} to prove termination of
-recursive functions on datatypes.
+@{text "size :: t \<Rightarrow> nat"} belonging to the @{text size} type class. The
+\keyw{fun} command relies on @{const size} to prove termination of recursive
+functions on datatypes.
 
 The plugin derives the following properties:
 
@@ -3209,8 +3209,20 @@
 
 \end{description}
 \end{indentblock}
+
+The @{text "t.size"} and @{text "t.size_t"} functions generated for datatypes
+defined by nested recursion through a datatype @{text u} depend on
+@{text "u.size_u"}.
+
+If the recursion is through a non-datatype @{text u} with type arguments
+@{text "'a\<^sub>1, \<dots>, 'a\<^sub>m"}, by default @{text u} values are given a size of 0. This
+can be improved upon by registering a custom size function of type
+@{text "('a\<^sub>1 \<Rightarrow> nat) \<Rightarrow> \<dots> \<Rightarrow> ('a\<^sub>m \<Rightarrow> nat) \<Rightarrow> u \<Rightarrow> nat"} using
+@{ML BNF_LFP_Size.register_size} or @{ML BNF_LFP_Size.register_size_global}. See
+@{file "~~/src/HOL/Library/Multiset.thy"} for an example.
 *}
 
+
 subsection {* Transfer
   \label{ssec:transfer} *}