# HG changeset patch
# User blanchet
# Date 1443717888 -7200
# Node ID af6b8bd0d07656276d3cbb4cfed793597b0f1f4f
# Parent  9f9b088d882456f046d630d87944cd4968a406a9
tuned datatype docs

diff -r 9f9b088d8824 -r af6b8bd0d076 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Oct 01 17:35:28 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Oct 01 18:44:48 2015 +0200
@@ -1,4 +1,5 @@
 (*  Title:      Doc/Datatypes/Datatypes.thy
+    Author:     Julian Biendarra, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Martin Desharnais, Ecole de technologie superieure
     Author:     Lorenz Panny, TU Muenchen
@@ -2737,7 +2738,7 @@
     next
       fix F :: "('d, 'a) fn" and f g :: "'a \<Rightarrow> 'b"
       assume "\<And>x. x \<in> set_fn F \<Longrightarrow> f x = g x"
-      thus "map_fn f F = map_fn g F"
+      then show "map_fn f F = map_fn g F"
         by transfer auto
     next
       fix f :: "'a \<Rightarrow> 'b"
@@ -2792,62 +2793,77 @@
 for further examples of BNF registration, some of which feature custom
 witnesses.
 
-For many typedefs (in particular for type copies) lifting the BNF structure
-from the raw type to the abstract type can be done uniformly. This is the task
-of the @{command lift_bnf} command. Using @{command lift_bnf} the above
-registration of @{typ "('d, 'a) fn"} as a BNF becomes much shorter.
+For many typedefs, lifting the BNF structure from the raw type to the abstract
+type can be done uniformly. This is the task of the @{command lift_bnf} command.
+Using @{command lift_bnf}, the above registration of @{typ "('d, 'a) fn"} as a
+BNF becomes much shorter:
 *}
 
-    (*<*) context early begin (*>*)
-    lift_bnf (*<*)(no_warn_wits)(*>*) ('d, 'a) fn by auto
-    (*<*) end (*>*)
+(*<*)
+    context early
+    begin
+(*>*)
+    lift_bnf (*<*)(no_warn_wits) (*>*)('d, 'a) fn
+      by auto
+(*<*)
+    end
+(*>*)
 
 text {*
-Indeed, for type copies the proof obligations are so simple that they can be
-discharged automatically, yielding another command @{command copy_bnf} which
-does not issue proof obligations.
+For type copies (@{command typedef}s with @{term UNIV} as the representing set),
+the proof obligations are so simple that they can be
+discharged automatically, yielding another command, @{command copy_bnf}, which
+does not emit any proof obligations:
 *}
 
-    (*<*) context late begin (*>*)
+(*<*)
+    context late
+    begin
+(*>*)
     copy_bnf ('d, 'a) fn
-    (*<*) end (*>*)
+(*<*)
+    end
+(*>*)
 
 text {*
-Since records (or rather record schemes) are particular type copies,
-the @{command copy_bnf} can be used to register records as BNFs.
+Since record schemas are type copies, @{command copy_bnf} can be used to
+register them as BNFs:
 *}
 
     record 'a point =
       xval :: 'a
       yval :: 'a
+
+text {* \blankline *}
     
     copy_bnf ('a, 'z) point_ext
 
 text {*
-The proof obligations handed over to the user by @{command lift_bnf} in
-the general case are simpler than the acual BNF properties (in particular,
-no cardinality reasoning is required). They are best illustrated on an
-example. Suppose we define the type of nonempty lists.
+In the general case, the proof obligations generated by @{command lift_bnf} are
+simpler than the acual BNF properties. In particular, no cardinality reasoning
+is required. Consider the following type of nonempty lists:
 *}
 
     typedef 'a nonempty_list = "{xs :: 'a list. xs \<noteq> []}" by auto
 
 text {*
-Then, @{command lift_bnf} requires us to prove that the set of nonempty lists
-is closed under the map function and the zip function (where the latter only
+The @{command lift_bnf} command requires us to prove that the set of nonempty lists
+is closed under the map function and the zip function. The latter only
 occurs implicitly in the goal, in form of the variable
-@{term "zs :: ('a \<times> 'b) list"}).
+@{term "zs :: ('a \<times> 'b) list"}.
 *}
 
-    lift_bnf (*<*)(no_warn_wits)(*>*) 'a nonempty_list
+    lift_bnf (*<*)(no_warn_wits) (*>*)'a nonempty_list
     proof -
       fix f and xs :: "'a list"
       assume "xs \<in> {xs. xs \<noteq> []}"
-      then show "map f xs \<in> {xs. xs \<noteq> []}" by (cases xs(*<*)rule: list.exhaust(*>*)) auto
+      then show "map f xs \<in> {xs. xs \<noteq> []}"
+        by (cases xs(*<*) rule: list.exhaust(*>*)) auto
     next
       fix zs :: "('a \<times> 'b) list"
       assume "map fst zs \<in> {xs. xs \<noteq> []}" "map snd zs \<in> {xs. xs \<noteq> []}"
-      then show "zs \<in> {xs. xs \<noteq> []}" by (cases zs(*<*)rule: list.exhaust(*>*)) auto
+      then show "zs \<in> {xs. xs \<noteq> []}"
+        by (cases zs (*<*)rule: list.exhaust(*>*)) auto
     qed
 
 text {*
@@ -2905,13 +2921,12 @@
 %%% TODO: elaborate on proof obligations
 *}
 
-subsubsection {* \keyw{lift_bnf} and \keyw{copy_bnf}
+subsubsection {* \keyw{lift_bnf}
   \label{sssec:lift-bnf} *}
 
 text {*
 \begin{matharray}{rcl}
-  @{command_def "lift_bnf"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
-  @{command_def "copy_bnf"} & : & @{text "local_theory \<rightarrow> local_theory"}
+  @{command_def "lift_bnf"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
 \end{matharray}
 
 @{rail \<open>
@@ -2922,30 +2937,45 @@
   @{syntax_def lb_options}: '(' ((@{syntax plugins} | 'no_warn_wits') + ',') ')'
   ;
   @{syntax_def wit_terms}: '[' 'wits' ':' terms ']'
-  ;
+\<close>}
+\medskip
+
+\noindent
+The @{command lift_bnf} command registers as a BNF an existing type (the
+\emph{abstract type}) that was defined as a subtype of a BNF (the \emph{raw
+type}) using the @{command typedef} command. To achieve this, it lifts the BNF
+structure on the raw type to the abstract type following a @{term
+type_definition} theorem. The theorem is usually inferred from the type, but can
+also be explicitly supplied by means of the optional @{text via} clause. In
+addition, custom names for the set functions, the map function, and the relator,
+as well as nonemptiness witnesses can be specified.
+
+Nonemptiness witnesses are not lifted from the raw type's BNF, as this would be
+incomplete. They must be given as terms (on the raw type) and proved to be
+witnesses. The command warns about witness types that are present in the raw
+type's BNF but not supplied by the user. The warning can be disabled by
+specifying the @{text no_warn_wits} option.
+*}
+
+subsubsection {* \keyw{copy_bnf}
+  \label{sssec:copy-bnf} *}
+
+text {*
+\begin{matharray}{rcl}
+  @{command_def "copy_bnf"} & : & @{text "local_theory \<rightarrow> local_theory"}
+\end{matharray}
+
+@{rail \<open>
   @@{command copy_bnf} target? ('(' @{syntax plugins} ')')? \<newline>
     @{syntax tyargs} name ('via' @{syntax thmref})? @{syntax map_rel}?
 \<close>}
 \medskip
 
 \noindent
-The @{command lift_bnf} command registers an existing type (abstract type),
-defined as a subtype of a BNF (raw type) using the @{command typedef} command,
-as a BNF. To do so, it lifts the BNF structure on the raw type to the abstract
-type following a @{term type_definition} theorem (the theorem is usually inferred
-from the type, but can also be explicitly supplied by the user using the
-@{text via} slot). In addition, custom names for map, set functions, and the relator,
-as well as nonemptiness witnesses can be specified; otherwise, default versions are used.
-Nonemptiness witnesses are not lifted from the raw type's BNF (this would be
-inherently incomplete), but must be given as terms (on the raw type) and proved
-to be witnesses. The command warns aggresively about witness types that a present
-in the raw type's BNF but not supplied by the user. The warning can be turned off
-by passing the @{text no_warn_wits} option.
-
-The @{command copy_bnf} command, performes the same lifting for type copies
-(@{command typedef}s with @{term UNIV} as the representing set) without bothering
-the user with trivial proof obligations. (Here, all nonemptiness witnesses from the raw
-type's BNF can also be lifted without problems.)
+The @{command copy_bnf} command performs the same lifting as @{command lift_bnf}
+for type copies (@{command typedef}s with @{term UNIV} as the representing set),
+without requiring the user to discharge any proof obligations or provide
+nonemptiness witnesses.
 *}
 
 subsubsection {* \keyw{bnf_axiomatization}
diff -r 9f9b088d8824 -r af6b8bd0d076 src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex	Thu Oct 01 17:35:28 2015 +0200
+++ b/src/Doc/Datatypes/document/root.tex	Thu Oct 01 18:44:48 2015 +0200
@@ -60,11 +60,9 @@
 
 \title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
 Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL}
-\author{Jasmin Christian Blanchette,
-Martin Desharnais, \\
-Lorenz Panny,
-Andrei Popescu, and
-Dmitriy Traytel}
+\author{Julian Biendarra, Jasmin Christian Blanchette, \\
+Martin Desharnais, Lorenz Panny, \\
+Andrei Popescu, and Dmitriy Traytel}
 
 \urlstyle{tt}
 
@@ -77,10 +75,11 @@
 \noindent
 This tutorial describes the definitional package for datatypes and codatatypes,
 and for primitively recursive and corecursive functions, in Isabelle/HOL. The
-package provides these commands:
-\keyw{datatype}, \keyw{datatype_compat}, \keyw{primrec}, \keyw{codatatype},
-\keyw{primcorec}, \keyw{prim\-co\-recursive}, \keyw{bnf}, \keyw{bnf_axiomatization},
-\keyw{print_bnfs}, and \keyw{free_\allowbreak constructors}.
+following commands are provided:
+\keyw{datatype}, \keyw{datatype_\allowbreak compat}, \keyw{prim\-rec}, \keyw{co\-data\-type},
+\keyw{prim\-co\-rec}, \keyw{prim\-co\-recursive}, \keyw{bnf}, \keyw{lift_\allowbreak bnf},
+\keyw{copy_\allowbreak bnf}, \keyw{bnf_\allowbreak axiom\-atization},
+\keyw{print_\allowbreak bnfs}, and \keyw{free_\allowbreak constructors}.
 \end{abstract}
 \end{sloppy}