--- a/src/Doc/Isar_Ref/HOL_Specific.thy Mon Jul 06 19:33:30 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon Jul 06 19:49:34 2015 +0200
@@ -1427,7 +1427,6 @@
chapter \<open>Proof tools\<close>
-
section \<open>Lifting package \label{sec:lifting}\<close>
text \<open>
@@ -1474,7 +1473,8 @@
;
@@{command (HOL) lifting_update} @{syntax nameref}
;
- @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?
+ @@{attribute (HOL) lifting_restore}
+ @{syntax thmref} (@{syntax thmref} @{syntax thmref})?
\<close>}
\begin{description}
@@ -1488,28 +1488,28 @@
command to work with the abstract type. An optional theorem @{term "reflp
R"}, which certifies that the equivalence relation R is total, can be
provided as a second argument. This allows the package to generate
- stronger transfer rules. And finally, the parametricity theorem for R can
- be provided as a third argument. This allows the package to generate a
- stronger transfer rule for equality.
+ stronger transfer rules. And finally, the parametricity theorem for @{term
+ R} can be provided as a third argument. This allows the package to
+ generate a stronger transfer rule for equality.
Users generally will not prove the @{text Quotient} theorem manually for
new types, as special commands exist to automate the process.
- When a new subtype is defined by @{command (HOL) typedef}, @{command (HOL)
- "lift_definition"} can be used in its second mode, where only the
- type_definition theorem @{text "type_definition Rep Abs A"} is used as an
- argument of the command. The command internally proves the corresponding
- Quotient theorem and registers it with @{command (HOL) setup_lifting}
- using its first mode.
+ \medskip When a new subtype is defined by @{command (HOL) typedef},
+ @{command (HOL) "lift_definition"} can be used in its second mode, where
+ only the @{term type_definition} theorem @{term "type_definition Rep Abs
+ A"} is used as an argument of the command. The command internally proves
+ the corresponding @{term Quotient} theorem and registers it with @{command
+ (HOL) setup_lifting} using its first mode.
For quotients, the command @{command (HOL) quotient_type} can be used. The
command defines a new quotient type and similarly to the previous case,
the corresponding Quotient theorem is proved and registered by @{command
(HOL) setup_lifting}.
- The command @{command (HOL) "setup_lifting"} also sets up the code
- generator for the new type. Later on, when a new constant is defined by
- @{command (HOL) "lift_definition"}, the Lifting package proves and
+ \medskip The command @{command (HOL) "setup_lifting"} also sets up the
+ code generator for the new type. Later on, when a new constant is defined
+ by @{command (HOL) "lift_definition"}, the Lifting package proves and
registers a code equation (if there is one) for the new constant.
\item @{command (HOL) "lift_definition"} @{text "f :: \<tau>"} @{keyword (HOL)
@@ -1518,15 +1518,15 @@
representation type. More formally, if @{text "t :: \<sigma>"}, then the command
builds a term @{text "F"} as a corresponding combination of abstraction
and representation functions such that @{text "F :: \<sigma> \<Rightarrow> \<tau>" } and defines
- @{text f} is as @{text "f \<equiv> F t"}. The term @{text t} does not have to be
- necessarily a constant but it can be any term.
-
- The command opens a proof environment and the user must discharge a
- respectfulness proof obligation. For a type copy, i.e., a typedef with
- @{text UNIV}, the obligation is discharged automatically. The proof goal
- is presented in a user-friendly, readable form. A respectfulness theorem
- in the standard format @{text f.rsp} and a transfer rule @{text
- f.transfer} for the Transfer package are generated by the package.
+ @{text "f \<equiv> F t"}. The term @{text t} does not have to be necessarily a
+ constant but it can be any term.
+
+ The command opens a proof and the user must discharge a respectfulness
+ proof obligation. For a type copy, i.e.\ a typedef with @{text UNIV}, the
+ obligation is discharged automatically. The proof goal is presented in a
+ user-friendly, readable form. A respectfulness theorem in the standard
+ format @{text f.rsp} and a transfer rule @{text f.transfer} for the
+ Transfer package are generated by the package.
The user can specify a parametricity theorems for @{text t} after the
keyword @{keyword "parametric"}, which allows the command to generate
@@ -1540,24 +1540,31 @@
unconditional for total quotients. The equation defines @{text f} using
the abstraction function.
- Integration with [@{attribute code} abstract]: For subtypes (e.g.,
- corresponding to a datatype invariant, such as @{typ "'a dlist"}),
+ \medskip Integration with [@{attribute code} abstract]: For subtypes
+ (e.g.\ corresponding to a datatype invariant, such as @{typ "'a dlist"}),
@{command (HOL) "lift_definition"} uses a code certificate theorem @{text
f.rep_eq} as a code equation. Because of the limitation of the code
generator, @{text f.rep_eq} cannot be used as a code equation if the
- subtype occurs inside the result type rather than at the top level (e.g.,
- function returning @{typ "'a dlist option"} vs. @{typ "'a dlist"}). In
- this case, an extension of @{command (HOL) "lift_definition"} can be
+ subtype occurs inside the result type rather than at the top level (e.g.\
+ function returning @{typ "'a dlist option"} vs. @{typ "'a dlist"}).
+
+ In this case, an extension of @{command (HOL) "lift_definition"} can be
invoked by specifying the flag @{text "code_dt"}. This extension enables
code execution through series of internal type and lifting definitions if
the return type @{text "\<tau>"} meets the following inductive conditions:
- \begin{description} \item @{text "\<tau>"} is a type variable \item @{text "\<tau> =
- \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"}, where @{text "\<kappa>"} is an abstract type constructor and
- @{text "\<tau>\<^sub>1 \<dots> \<tau>\<^sub>n"} do not contain abstract types (i.e., @{typ "int
- dlist"} is allowed whereas @{typ "int dlist dlist"} not) \item @{text "\<tau> =
- \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"}, @{text "\<kappa>"} is a type constructor that was defined as a
- (co)datatype whose constructor argument types do not contain either
- non-free datatypes or the function type. \end{description}
+
+ \begin{description}
+
+ \item @{text "\<tau>"} is a type variable \item @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"},
+ where @{text "\<kappa>"} is an abstract type constructor and @{text "\<tau>\<^sub>1 \<dots> \<tau>\<^sub>n"}
+ do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed whereas
+ @{typ "int dlist dlist"} not)
+
+ \item @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"}, @{text "\<kappa>"} is a type constructor that
+ was defined as a (co)datatype whose constructor argument types do not
+ contain either non-free datatypes or the function type.
+
+ \end{description}
Integration with [@{attribute code} equation]: For total quotients,
@{command (HOL) "lift_definition"} uses @{text f.abs_eq} as a code
@@ -1592,7 +1599,7 @@
\item @{command (HOL) "print_quotients"} prints stored quotient theorems.
\item @{attribute (HOL) quot_map} registers a quotient map theorem, a
- theorem showing how to "lift" quotients over type constructors. E.g.,
+ theorem showing how to "lift" quotients over type constructors. E.g.\
@{term "Quotient R Abs Rep T \<Longrightarrow> Quotient (rel_set R) (image Abs) (image
Rep) (rel_set T)"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"}
or @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically
@@ -1600,7 +1607,7 @@
\item @{attribute (HOL) relator_eq_onp} registers a theorem that shows
that a relator applied to an equality restricted by a predicate @{term P}
- (i.e., @{term "eq_onp P"}) is equal to a predicator applied to the @{term
+ (i.e.\ @{term "eq_onp P"}) is equal to a predicator applied to the @{term
P}. The combinator @{const eq_onp} is used for internal encoding of proper
subtypes. Such theorems allows the package to hide @{text eq_onp} from a
user in a user-readable form of a respectfulness theorem. For examples see
@@ -1609,7 +1616,7 @@
dead variables.
\item @{attribute (HOL) "relator_mono"} registers a property describing a
- monotonicity of a relator. E.g., @{term "A \<le> B \<Longrightarrow> rel_set A \<le> rel_set B"}.
+ monotonicity of a relator. E.g.\ @{prop "A \<le> B \<Longrightarrow> rel_set A \<le> rel_set B"}.
This property is needed for proving a stronger transfer rule in
@{command_def (HOL) "lift_definition"} when a parametricity theorem for
the raw term is specified and also for the reflexivity prover. For
@@ -1618,11 +1625,11 @@
involved type is BNF without dead variables.
\item @{attribute (HOL) "relator_distr"} registers a property describing a
- distributivity of the relation composition and a relator. E.g., @{text
+ distributivity of the relation composition and a relator. E.g.\ @{text
"rel_set R \<circ>\<circ> rel_set S = rel_set (R \<circ>\<circ> S)"}. This property is needed for
proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}
when a parametricity theorem for the raw term is specified. When this
- equality does not hold unconditionally (e.g., for the function type), the
+ equality does not hold unconditionally (e.g.\ for the function type), the
user can specified each direction separately and also register multiple
theorems with different set of assumptions. This attribute can be used
only after the monotonicity property was already registered by @{attribute
@@ -1643,7 +1650,7 @@
Lifting infrastructure and thus sets up lifting for an abstract type
@{text \<tau>} (that is defined by @{text Quotient_thm}). Optional theorems
@{text pcr_def} and @{text pcr_cr_eq_thm} can be specified to register the
- parametrized correspondence relation for @{text \<tau>}. E.g., for @{typ "'a
+ parametrized correspondence relation for @{text \<tau>}. E.g.\ for @{typ "'a
dlist"}, @{text pcr_def} is @{text "pcr_dlist A \<equiv> list_all2 A \<circ>\<circ>
cr_dlist"} and @{text pcr_cr_eq_thm} is @{text "pcr_dlist op= = op="}.
This attribute is rather used for low-level manipulation with set-up of
@@ -1703,7 +1710,7 @@
theorem as @{method (HOL) "transfer"} internally does.
\item @{attribute (HOL) Transfer.transferred} works in the opposite
- direction than @{method (HOL) "transfer'"}. E.g., given the transfer
+ direction than @{method (HOL) "transfer'"}. E.g.\ given the transfer
relation @{text "ZN x n \<equiv> (x = int n)"}, corresponding transfer rules and
the theorem @{text "\<forall>x::int \<in> {0..}. x < x + 1"}, the attribute would
prove @{text "\<forall>n::nat. n < n + 1"}. The attribute is still in experimental
@@ -1731,10 +1738,10 @@
\item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a
collection of rules, which specify a domain of a transfer relation by a
- predicate. E.g., given the transfer relation @{text "ZN x n \<equiv> (x = int
+ predicate. E.g.\ given the transfer relation @{text "ZN x n \<equiv> (x = int
n)"}, one can register the following transfer domain rule: @{text "Domainp
ZN = (\<lambda>x. x \<ge> 0)"}. The rules allow the package to produce more readable
- transferred goals, e.g., when quantifiers are transferred.
+ transferred goals, e.g.\ when quantifiers are transferred.
\item @{attribute (HOL) relator_eq} attribute collects identity laws for
relators of various type constructors, e.g. @{term "rel_set (op =) = (op
@@ -1745,7 +1752,7 @@
dead variables.
\item @{attribute_def (HOL) "relator_domain"} attribute collects rules
- describing domains of relators by predicators. E.g., @{term "Domainp
+ describing domains of relators by predicators. E.g.\ @{term "Domainp
(rel_set T) = (\<lambda>A. Ball A (Domainp T))"}. This allows the package to lift
transfer domain rules through type constructors. For examples see @{file
"~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This
@@ -2153,7 +2160,7 @@
an argument to tester, making @{text "tester ="} optional. When
multiple testers are given, these are applied in parallel. If no
tester is specified, quickcheck uses the testers that are set
- active, i.e., configurations @{attribute
+ active, i.e.\ configurations @{attribute
quickcheck_exhaustive_active}, @{attribute
quickcheck_random_active}, @{attribute
quickcheck_narrowing_active} are set to true.
@@ -2183,7 +2190,7 @@
structured proofs should be ignored.
\item[@{text locale}] specifies how to process conjectures in
- a locale context, i.e., they can be interpreted or expanded.
+ a locale context, i.e.\ they can be interpreted or expanded.
The option is a whitespace-separated list of the two words
@{text interpret} and @{text expand}. The list determines the
order they are employed. The default setting is to first use