# 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 \ 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 \ 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, \, '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 \ nat) \ \ \ ('a\<^sub>m \ nat) \ u \ 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} *}