summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | kuncar |

Wed, 30 Jul 2014 16:44:54 +0200 | |

changeset 57829 | b1113689622b |

parent 57828 | bf3bdb9240c2 |

child 57830 | 2d0f0d6fdf3e |

update documentation for Lifting/Transfer

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