--- a/src/Doc/Isar_Ref/HOL_Specific.thy Wed Jul 30 16:44:54 2014 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Wed Jul 30 16:44:54 2014 +0200
@@ -1542,6 +1542,10 @@
@{text "bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"}\\
@{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)"}
+ Preservation of predicates on relations (@{text "bi_unique, bi_total,
+ right_unique, right_total, left_unique, left_total"}) with the respect to a relator
+ is proved automatically if the involved type is BNF\cite{isabelle-datatypes} without dead variables.
+
\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 n)"},
@@ -1550,15 +1554,19 @@
more readable 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. @{text "list_all2
+ for relators of various type constructors, e.g. @{term "rel_set
(op =) = (op =)"}. The @{method (HOL) transfer} method uses these
lemmas to infer transfer rules for non-polymorphic constants on
- the fly.
+ the fly. For examples see @{file
+ "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+ This property is proved automatically if the involved type is BNF without dead variables.
\item @{attribute_def (HOL) "relator_domain"} attribute collects rules
- describing domains of relators by predicators. E.g., @{text "Domainp A = P \<Longrightarrow>
- Domainp (list_all2 A) = (list_all P)"}. This allows the package to lift transfer
- domain rules through type constructors.
+ 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 property is proved automatically if the involved type is BNF without dead variables.
\end{description}
@@ -1603,7 +1611,7 @@
@{rail \<open>
@@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \<newline>
- 'is' @{syntax term} (@'parametric' @{syntax thmref})?;
+ 'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?;
\<close>}
@{rail \<open>
@@ -1625,10 +1633,10 @@
The command supports two modes. The first one is a low-level mode when
the user must provide as a first
argument of @{command (HOL) "setup_lifting"} a
- quotient theorem @{text "Quotient R Abs Rep T"}. The
+ quotient theorem @{term "Quotient R Abs Rep T"}. The
package configures a transfer rule for equality, a domain transfer
rules and sets up the @{command_def (HOL) "lift_definition"}
- command to work with the abstract type. An optional theorem @{text "reflp R"}, which certifies that
+ 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.
@@ -1671,9 +1679,9 @@
@{text f.transfer} for the Transfer package are generated by the
package.
- The user can specify a parametricity theorem for @{text t} after the keyword
+ The user can specify a parametricity theorems for @{text t} after the keyword
@{keyword "parametric"}, which allows the command
- to generate a parametric transfer rule for @{text f}.
+ to generate parametric transfer rules for @{text f}.
For each constant defined through trivial quotients (type copies or
subtypes) @{text f.rep_eq} is generated. The equation is a code certificate
@@ -1720,38 +1728,42 @@
theorems.
\item @{attribute (HOL) quot_map} registers a quotient map
- theorem. E.g., @{text "Quotient R Abs Rep T \<Longrightarrow>
- Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"}.
+ theorem, a 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/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
- in the same directory.
+ "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+ This property is proved automatically if the involved type is BNF without dead variables.
\item @{attribute (HOL) relator_eq_onp} registers a theorem that
- shows a relationship between the constant @{text
- eq_onp} (used for internal encoding of proper subtypes)
- and a relator. Such theorems allows the package to hide @{text
+ 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 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 @{file
- "~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.
+ "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+ This property is proved automatically if the involved type is BNF without dead variables.
\item @{attribute (HOL) "relator_mono"} registers a property describing a monotonicity of a relator.
- E.g., @{text "A \<le> B \<Longrightarrow> list_all2 A \<le> list_all2 B"}. For examples
- see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"}
- or Lifting_*.thy files in the same directory.
+ E.g., @{term "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.
+ when a parametricity theorem for the raw term is specified and also for the reflexivity prover.
+ For examples see @{file
+ "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+ This property is proved automatically if the 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 "list_all2 R \<circ>\<circ> list_all2 S = list_all2 (R \<circ>\<circ> S)"}.
+ @{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 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 (HOL) "relator_mono"}. For examples
- see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"}
- or Lifting_*.thy files in the same directory.
+ @{attribute (HOL) "relator_mono"}. For examples see @{file
+ "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+ This property is proved automatically if the involved type is BNF without dead variables.
\item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem
from the Lifting infrastructure and thus de-register the corresponding quotient.
@@ -1773,6 +1785,14 @@
together with the commands @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} is
preferred for normal usage.
+ \item Integration with the BNF package\cite{isabelle-datatypes}:
+ As already mentioned, the theorems that are registered
+ by the following attributes are proved and registered automatically if the involved type
+ is BNF without dead variables: @{attribute (HOL) quot_map}, @{attribute (HOL) relator_eq_onp},
+ @{attribute (HOL) "relator_mono"}, @{attribute (HOL) "relator_distr"}. Also the definition of a
+ relator and predicator is provided automatically. Moreover, if the BNF represents a datatype,
+ simplification rules for a predicator are again proved automatically.
+
\end{description}
*}