--- 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}