# HG changeset patch # User kuncar # Date 1381755697 -7200 # Node ID 409d7f7247f4c12a0b20758f1b1cc56c1680ab61 # Parent ce028cf2e58e9562c17ccc200a18c70e4212e95e update documentation of Lifting/Transfer and Quotient diff -r ce028cf2e58e -r 409d7f7247f4 src/Doc/IsarRef/HOL_Specific.thy --- a/src/Doc/IsarRef/HOL_Specific.thy Fri Oct 11 18:36:51 2013 +0200 +++ b/src/Doc/IsarRef/HOL_Specific.thy Mon Oct 14 15:01:37 2013 +0200 @@ -1259,17 +1259,18 @@ \end{matharray} The quotient package defines a new quotient type given a raw type - and a partial equivalence relation. It also includes automation for - transporting definitions and theorems. It can automatically produce - definitions and theorems on the quotient type, given the - corresponding constants and facts on the raw type. + and a partial equivalence relation. The package also historically + includes automation for transporting definitions and theorems. + But most of this automation was superseded by the Lifting and Transfer + packages. The user should consider using these two new packages for + lifting definitions and transporting theorems. @{rail " @@{command (HOL) quotient_type} (spec); spec: @{syntax typespec} @{syntax mixfix}? '=' \\ @{syntax type} '/' ('partial' ':')? @{syntax term} \\ - (@'morphisms' @{syntax name} @{syntax name})?; + (@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})?; "} @{rail " @@ -1289,9 +1290,9 @@ \begin{description} - \item @{command (HOL) "quotient_type"} defines quotient types. The + \item @{command (HOL) "quotient_type"} defines a new quotient type @{text \}. The injection from a quotient type to a raw type is called @{text - rep_t}, its inverse @{text abs_t} unless explicit @{keyword (HOL) + rep_\}, its inverse @{text abs_\} unless explicit @{keyword (HOL) "morphisms"} specification provides alternative names. @{command (HOL) "quotient_type"} requires the user to prove that the relation is an equivalence relation (predicate @{text equivp}), unless the @@ -1300,6 +1301,22 @@ partial} is weaker in the sense that less things can be proved automatically. + The command internally proves a Quotient theorem and sets up the Lifting + package by the command @{command (HOL) setup_lifting}. Thus the Lifting + and Transfer packages can be used also with quotient types defined by + @{command (HOL) "quotient_type"} without any extra set-up. The parametricity + theorem for the equivalence relation R can be provided as an extra argument + of the command and is passed to the corresponding internal call of @{command (HOL) setup_lifting}. + This theorem allows the Lifting package to generate a stronger transfer rule for equality. + + \end{description} + + The most of the rest of the package was superseded by the Lifting and Transfer + packages. The user should consider using these two new packages for + lifting definitions and transporting theorems. + + \begin{description} + \item @{command (HOL) "quotient_definition"} defines a constant on the quotient type. @@ -1497,8 +1514,12 @@ @{method_def (HOL) "transfer"} & : & @{text method} \\ @{method_def (HOL) "transfer'"} & : & @{text method} \\ @{method_def (HOL) "transfer_prover"} & : & @{text method} \\ + @{attribute_def (HOL) "Transfer.transferred"} & : & @{text attribute} \\ + @{attribute_def (HOL) "untransferred"} & : & @{text attribute} \\ @{attribute_def (HOL) "transfer_rule"} & : & @{text attribute} \\ + @{attribute_def (HOL) "transfer_domain_rule"} & : & @{text attribute} \\ @{attribute_def (HOL) "relator_eq"} & : & @{text attribute} \\ + @{attribute_def (HOL) "relator_domain"} & : & @{text attribute} \\ \end{matharray} \begin{description} @@ -1524,6 +1545,16 @@ rules. It should be applied after unfolding the constant definitions. + \item @{attribute (HOL) "untransferred"} proves the same equivalent 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 + relation @{text "ZN x n \ (x = int n)"}, corresponding transfer rules and the theorem + @{text "\x::int \ {0..}. x < x + 1"}, the attribute would prove + @{text "\n::nat. n < n + 1"}. The attribute is still in experimental + phase of development. + \item @{attribute (HOL) "transfer_rule"} attribute maintains a collection of transfer rules, which relate constants at two different types. Typical transfer rules may relate different type @@ -1540,83 +1571,140 @@ @{text "bi_unique A \ (list_all2 A ===> op =) distinct distinct"}\\ @{text "\bi_unique A; bi_unique B\ \ bi_unique (prod_rel A B)"} + \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 \ (x = int n)"}, + one can register the following transfer domain rule: + @{text "Domainp ZN = (\x. x \ 0)"}. The rules allow the package to produce + 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 (op =) = (op =)"}. The @{method (HOL) transfer} method uses these lemmas to infer transfer rules for non-polymorphic constants on the fly. + \item @{attribute_def (HOL) "relator_domain"} attribute collects rules + describing domains of relators by predicators. E.g., @{text "Domainp A = P \ + Domainp (list_all2 A) = (list_all P)"}. This allows the package to lift transfer + domain rules through type constructors. + \end{description} + Theoretical background can be found in \cite{Huffman-Kuncar:2013:lifting_transfer}. *} section {* Lifting package *} text {* + The Lifting package allows users to lift terms of the raw type to the abstract type, which is + a necessary step in building a library for an abstract type. Lifting defines a new constant + by combining coercion functions (Abs and Rep) with the raw term. It also proves an appropriate + transfer rule for the Transfer package and, if possible, an equation for the code generator. + + The Lifting package provides two main commands: @{command (HOL) "setup_lifting"} for initializing + the package to work with a new type, and @{command (HOL) "lift_definition"} for lifting constants. + The Lifting package works with all four kinds of type abstraction: type copies, subtypes, + total quotients and partial quotients. + + Theoretical background can be found in \cite{Huffman-Kuncar:2013:lifting_transfer}. + \begin{matharray}{rcl} @{command_def (HOL) "setup_lifting"} & : & @{text "local_theory \ local_theory"}\\ @{command_def (HOL) "lift_definition"} & : & @{text "local_theory \ proof(prove)"}\\ + @{command_def (HOL) "lifting_forget"} & : & @{text "local_theory \ local_theory"}\\ + @{command_def (HOL) "lifting_update"} & : & @{text "local_theory \ local_theory"}\\ @{command_def (HOL) "print_quot_maps"} & : & @{text "context \"}\\ @{command_def (HOL) "print_quotients"} & : & @{text "context \"}\\ @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\ @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\ @{attribute_def (HOL) "reflexivity_rule"} & : & @{text attribute} \\ - @{attribute_def (HOL) "quot_del"} & : & @{text attribute} + @{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\ + @{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\ + @{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\ + @{attribute_def (HOL) "lifting_restore"} & : & @{text attribute} \\ \end{matharray} @{rail " @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \\ - @{syntax thmref} @{syntax thmref}?; + @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?; "} @{rail " @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \\ - 'is' @{syntax term}; + 'is' @{syntax term} (@'parametric' @{syntax thmref})?; + "} + + @{rail " + @@{command (HOL) lifting_forget} @{syntax nameref}; + "} + + @{rail " + @@{command (HOL) lifting_update} @{syntax nameref}; + "} + + @{rail " + @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?; "} \begin{description} \item @{command (HOL) "setup_lifting"} Sets up the Lifting package - to work with a user-defined type. The user must provide either a - quotient theorem @{text "Quotient R Abs Rep T"} or a - type_definition theorem @{text "type_definition Rep Abs A"}. The - package configures transfer rules for equality and quantifiers on - the type, and sets up the @{command_def (HOL) "lift_definition"} - command to work with the type. In the case of a quotient theorem, - an optional theorem @{text "reflp R"} can be provided as a second - argument. This allows the package to generate stronger transfer - rules. - - @{command (HOL) "setup_lifting"} is called automatically if a - quotient type is defined by the command @{command (HOL) - "quotient_type"} from the Quotient package. - - If @{command (HOL) "setup_lifting"} is called with a - type_definition theorem, the abstract type implicitly defined by - the theorem is declared as an abstract type in the code - generator. This allows @{command (HOL) "lift_definition"} to - register (generated) code certificate theorems as abstract code - equations in the code generator. The option @{text "no_code"} - of the command @{command (HOL) "setup_lifting"} can turn off that - behavior and causes that code certificate theorems generated by - @{command (HOL) "lift_definition"} are not registered as abstract - code equations. - - \item @{command (HOL) "lift_definition"} @{text "f :: \ is t"} + to work with a user-defined type. + 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 + 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 + 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. + + 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. + + 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 registers a code equation (if there is one) for the new constant. + If the option @{text "no_code"} is specified, the Lifting package does not set up the code + generator and as a consequence no code equations involving an abstract type are registered + by @{command (HOL) "lift_definition"}. + + \item @{command (HOL) "lift_definition"} @{text "f :: \"} @{keyword (HOL) "is"} @{text t} Defines a new function @{text f} with an abstract type @{text \} in terms of a corresponding operation @{text t} on a - representation type. The term @{text t} doesn't have to be - necessarily a constant but it can be any term. - - Users must discharge a respectfulness proof obligation when each - constant is defined. For a type copy, i.e. a typedef with @{text - UNIV}, the proof is discharged automatically. The obligation is + representation type. More formally, if @{text "t :: \"}, then + the command builds a term @{text "F"} as a corresponding combination of abstraction + and representation functions such that @{text "F :: \ \ \" } and + defines @{text f} is as @{text "f \ 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.tranfer} for the Transfer package are generated by the + @{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 + @{keyword "parametric"}, which allows the command + to generate a parametric transfer rule 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 that defines @{text f} using the representation function. @@ -1625,14 +1713,36 @@ for total quotients. The equation defines @{text f} using the abstraction function. - Integration with code_abstype: For subtypes (e.g., + Integration with [@{attribute code} abstract]: For subtypes (e.g., corresponding to a datatype invariant, such as dlist), @{command (HOL) "lift_definition"} uses a code certificate theorem @{text f.rep_eq} as a code equation. - Integration with code: For total quotients, @{command + Integration with [@{attribute code} equation]: For total quotients, @{command (HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation. + \item @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} + These two commands serve for storing and deleting the set-up of + the Lifting package and corresponding transfer rules defined by this package. + This is useful for hiding of type construction details of an abstract type + when the construction is finished but it still allows additions to this construction + when this is later necessary. + + Whenever the Lifting package is set up with a new abstract type @{text "\"} by + @{command_def (HOL) "lift_definition"}, the package defines a new bundle + that is called @{text "\.lifting"}. This bundle already includes set-up for the Lifting package. + The new transfer rules + introduced by @{command (HOL) "lift_definition"} can be stored in the bundle by + the command @{command (HOL) "lifting_update"} @{text "\.lifting"}. + + The command @{command (HOL) "lifting_forget"} @{text "\.lifting"} deletes set-up of the Lifting + package + for @{text \} and deletes all the transfer rules that were introduced + by @{command (HOL) "lift_definition"} using @{text \} as an abstract type. + + The stored set-up in a bundle can be reintroduced by the Isar commands for including a bundle + (@{command "include"}, @{keyword "includes"} and @{command "including"}). + \item @{command (HOL) "print_quot_maps"} prints stored quotient map theorems. @@ -1640,9 +1750,11 @@ theorems. \item @{attribute (HOL) quot_map} registers a quotient map - theorem. For examples see @{file - "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy - files. + theorem. E.g., @{text "Quotient R Abs Rep T \ + Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"}. + For examples see @{file + "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files + in the same directory. \item @{attribute (HOL) invariant_commute} registers a theorem that shows a relationship between the constant @{text @@ -1650,20 +1762,54 @@ and a relator. Such theorems allows the package to hide @{text Lifting.invariant} from a user in a user-readable form of a respectfulness theorem. For examples see @{file - "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy - files. + "~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory. \item @{attribute (HOL) reflexivity_rule} registers a theorem that shows - that a relator respects reflexivity and left-totality. For examples - see @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy - The property is used in generation of abstraction function equations. + that a relator respects reflexivity, left-totality and left_uniqueness. For examples + see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files + in the same directory. + The property is used in a reflexivity prover, which is used for discharging respectfulness + theorems for type copies and also for discharging assumptions of abstraction function equations. + + \item @{attribute (HOL) "relator_mono"} registers a property describing a monotonicity of a relator. + E.g., @{text "A \ B \ list_all2 A \ 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. + 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. + + \item @{attribute (HOL) "relator_distr"} registers a property describing a distributivity + of the relation composition and a relator. E.g., + @{text "list_all2 R \\ list_all2 S = list_all2 (R \\ 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. \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem from the Lifting infrastructure and thus de-register the corresponding quotient. This effectively causes that @{command (HOL) lift_definition} will not - do any lifting for the corresponding type. It serves mainly for hiding - of type construction details when the construction is done. See for example - @{file "~~/src/HOL/Int.thy"}. + do any lifting for the corresponding type. This attribute is rather used for low-level + manipulation with set-up of the Lifting package because @{command (HOL) lifting_forget} is + preferred for normal usage. + + \item @{attribute (HOL) lifting_restore} @{text "Quotient_thm pcr_def pcr_cr_eq_thm"} + registers the Quotient theorem @{text Quotient_thm} in the Lifting infrastructure + and thus sets up lifting for an abstract type @{text \} (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 \}. E.g., for @{text "'a dlist"}, @{text pcr_def} is + @{text "pcr_dlist A \ list_all2 A \\ 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 the Lifting package because using of the bundle @{text \.lifting} + together with the commands @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} is + preferred for normal usage. + \end{description} *} @@ -2383,7 +2529,7 @@ ; @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') ) - ; + ;cite @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor | symbol_class | symbol_class_relation | symbol_class_instance diff -r ce028cf2e58e -r 409d7f7247f4 src/Doc/manual.bib --- a/src/Doc/manual.bib Fri Oct 11 18:36:51 2013 +0200 +++ b/src/Doc/manual.bib Mon Oct 14 15:01:37 2013 +0200 @@ -794,6 +794,16 @@ pages = {205-216}, publisher = {Elsevier}} +@inproceedings{Huffman-Kuncar:2013:lifting_transfer, + author = {Brian Huffman and Ond\v{r}ej Kun\v{c}ar}, + title = {{Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL}}, + booktitle = {Certified Programs and Proofs (CPP 2013)}, + year = 2013, + publisher = Springer, + series = {Lecture Notes in Computer Science}, + volume = {8307}, +} + @Book{Huth-Ryan-book, author = {Michael Huth and Mark Ryan}, title = {Logic in Computer Science. Modelling and reasoning about systems},