
diff -r 9d714be4f028 -r 89034dc40247 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Sep 05 00:41:01 2014 +0200
@@ -128,9 +128,9 @@
 %\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
 %describes the package's programmatic interface.
 
-%\item Section \ref{sec:interoperability}, ``Interoperability,''
-%is concerned with the packages' interaction with other Isabelle packages and
-%tools, such as the code generator and the counterexample generators.
+\item Section \ref{sec:plugins}, ``Plugins,''
+is concerned with the package's interoperability with other Isabelle packages
+and tools, such as Transfer, Lifting, and Quickcheck.
 
 %\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
 %Limitations,'' concludes with known open issues at the time of writing.
@@ -482,7 +482,9 @@
     (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \<newline>
      @{syntax map_rel}? (@'where' (prop + '|'))? + @'and')
   ;
-  @{syntax_def dt_options}: '(' (('discs_sels' | 'no_code') + ',') ')'
+  @{syntax_def plugins}: 'plugins' ('only' | 'del') ':' (name +)
+  ;
+  @{syntax_def dt_options}: '(' ((@{syntax plugins} | 'discs_sels' | 'no_code') + ',') ')'
   ;
   @{syntax_def map_rel}: @'for' ((('map' | 'rel') ':' name) +)
 \<close>}
@@ -497,13 +499,17 @@
 context (e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}),
 and \synt{prop} denotes a HOL proposition.
 
-The optional target is optionally followed by one or both of the following
+The optional target is optionally followed by a combination of the following
 options:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}
 
 \item
+The @{text "plugins"} option indicates which plugins should be enabled
+(@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
+
+\item
 The @{text "discs_sels"} option indicates that discriminators and selectors
 should be generated. The option is implicitly enabled if names are specified for
 discriminators or selectors.
@@ -536,7 +542,7 @@
 
 The optional names preceding the type variables allow to override the default
 names of the set functions (@{text set\<^sub>1_t}, \ldots, @{text set\<^sub>m_t}). Type
-arguments can be marked as dead by entering ``@{text dead}'' in front of the
+arguments can be marked as dead by entering @{text dead} in front of the
 type variable (e.g., ``@{text "(dead 'a)"}''); otherwise, they are live or dead
 (and a set function is generated or not) depending on where they occur in the
 right-hand sides of the definition. Declaring a type argument as dead can speed
@@ -659,9 +665,7 @@
 Relator: &
   @{text t.rel_t} \\
 Recursor: &
-  @{text t.rec_t} \\
-Size function: &
-  @{text t.size_t}
+  @{text t.rec_t}
 \end{tabular}
 
 \medskip
@@ -670,9 +674,6 @@
 The case combinator, discriminators, and selectors are collectively called
 \emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
 names and is normally hidden.
-
-In addition to the above, the @{class size} class is instantiated to overload the
-@{const size} function based on @{text t.size_t}.
 *}
 
 
@@ -1012,18 +1013,6 @@
 @{thm list.rec(1)[no_vars]} \\
 @{thm list.rec(2)[no_vars]}
 
-\item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
-@{thm list.rec_o_map[no_vars]}
-
-\item[@{text "t."}\hthm{size} @{text "[simp, code]"}\rm:] ~ \\
-@{thm list.size(1)[no_vars]} \\
-@{thm list.size(2)[no_vars]} \\
-@{thm list.size(3)[no_vars]} \\
-@{thm list.size(4)[no_vars]}
-
-\item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\
-@{thm list.size_o_map[no_vars]}
-
 \end{description}
 \end{indentblock}
 
@@ -1054,12 +1043,9 @@
 
 \item \emph{The Standard ML interfaces are different.} Tools and extensions
 written to call the old ML interfaces will need to be adapted to the new
-interfaces. This concerns Quickcheck in particular. Whenever possible, it is
-recommended to use @{command datatype_compat} to register new-style datatypes
-as old-style datatypes.
-
-\item \emph{The constants @{text t_case}, @{text t_rec}, and @{text t_size} are
-now called @{text case_t}, @{text rec_t}, and @{text size_t}.}
+interfaces. Whenever possible, it is recommended to use
+@{command datatype_compat} to register new-style datatypes as old-style
+datatypes.
 
 \item \emph{The recursor @{text rec_t} has a different signature for nested
 recursive datatypes.} In the old package, nested recursion through non-functions
@@ -1739,7 +1725,7 @@
 with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
 \ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
 datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
-recursor is replaced by a dual concept and no size function is produced:
+recursor is replaced by a dual concept:
 
 \medskip
 
@@ -2622,7 +2608,8 @@
 @{rail \<open>
   @@{command bnf} target? (name ':')? type \<newline>
     'map:' term ('sets:' (term +))? 'bd:' term \<newline>
-    ('wits:' (term +))? ('rel:' term)?
+    ('wits:' (term +))? ('rel:' term)? \<newline>
+    @{syntax plugins}?
 \<close>}
 
 \medskip
@@ -2650,8 +2637,9 @@
 \end{matharray}
 
 @{rail \<open>
-  @@{command bnf_axiomatization} target? @{syntax tyargs}? name \<newline>
-    @{syntax wit_types}? mixfix? @{syntax map_rel}?
+  @@{command bnf_axiomatization} target? @{syntax plugins}? \<newline>
+    @{syntax tyargs}? name @{syntax wit_types}? \<newline>
+    mixfix? @{syntax map_rel}?
   ;
   @{syntax_def wit_types}: '[' 'wits' ':' types ']'
 \<close>}
@@ -2669,7 +2657,7 @@
 parenthesized mixfix notation \cite{isabelle-isar-ref}.
 
 Type arguments are live by default; they can be marked as dead by entering
-``@{text dead}'' in front of the type variable (e.g., ``@{text "(dead 'a)"}'')
+@{text dead} in front of the type variable (e.g., ``@{text "(dead 'a)"}'')
 instead of an identifier for the corresponding set function. Witnesses can be
 specified by their types. Otherwise, the syntax of @{command bnf_axiomatization}
 is identical to the left-hand side of a @{command datatype_new} or
@@ -2779,35 +2767,78 @@
 *)
 
 
-(*
-section {* Interoperability
-  \label{sec:interoperability} *}
+section {* Plugins
+  \label{sec:plugins} *}
+
+text {*
+Plugins extend the (co)datatype package to interoperate with other Isabelle
+packages and tools, such as Transfer, Lifting, and Quickcheck. They can be
+enabled or disabled individually using the @{syntax plugins} option to
+@{command datatype_new}, @{command codatatype}, @{command free_constructors},
+@{command bnf}, and @{command bnf_axiomatization}. For example:
+*}
+
+    datatype_new (plugins del: size) color = Red | Black
+
+
+subsection {* Size
+  \label{ssec:size} *}
 
 text {*
-The package's interaction with other Isabelle packages and tools, such as the
-code generator and the counterexample generators.
+For each datatype, the @{text size} plugin generates a parameterized size
+function @{text "t.size_t"} as well as a specific instance
+@{text "size \<Colon> t \<Rightarrow> bool"} 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:
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{size} @{text "[simp, code]"}\rm:] ~ \\
+@{thm list.size(1)[no_vars]} \\
+@{thm list.size(2)[no_vars]} \\
+@{thm list.size(3)[no_vars]} \\
+@{thm list.size(4)[no_vars]}
+
+\item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
+@{thm list.rec_o_map[no_vars]}
+
+\item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\
+@{thm list.size_o_map[no_vars]}
+(This property is not generated for all datatypes.)
+
+\end{description}
+\end{indentblock}
 *}
 
 
-subsection {* Transfer and Lifting
-  \label{ssec:transfer-and-lifting} *}
-
-
-subsection {* Code Generator
-  \label{ssec:code-generator} *}
+subsection {* Transfer
+  \label{ssec:transfer} *}
+
+text {*
+The @{text transfer} plugin generates properties and attributes that guide the
+Transfer tool.
+*}
+
+
+subsection {* Lifting
+  \label{ssec:lifting} *}
+
+text {*
+The @{text lifting} plugin generates properties that guide the Lifting tool.
+*}
 
 
 subsection {* Quickcheck
   \label{ssec:quickcheck} *}
 
-
-subsection {* Nitpick
-  \label{ssec:nitpick} *}
-
-
-subsection {* Nominal Isabelle
-  \label{ssec:nominal-isabelle} *}
-*)
+text {*
+The integration with Quickcheck is accomplished by a number of plugins that
+instantiate specific type classes: @{text random}, @{text exhaustive},
+@{text bounded_forall}, @{text full_exhaustive}, @{text narrowing}.
+*}
 
 
 (*
@@ -2821,8 +2852,6 @@
 text {*
 %* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
 %
-%* partial documentation
-%
 %* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
 %  (for @{command datatype_compat} and prim(co)rec)
 %




