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

author | wenzelm |

Mon, 06 Jul 2015 21:36:52 +0200 | |

changeset 60677 | 7109b66ba151 |

parent 60676 | 92fd47ae2a67 |

child 60678 | 17ba2df56dee |

tuned;

--- a/src/Doc/Isar_Ref/HOL_Specific.thy Mon Jul 06 21:20:28 2015 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon Jul 06 21:36:52 2015 +0200 @@ -1387,28 +1387,33 @@ \begin{description} \item @{command (HOL) "setup_lifting"} Sets up the Lifting package 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 @{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 @{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 @{term - R} can be provided as a third argument. This allows the package to - generate a stronger transfer rule for equality. + with a user-defined type. The command supports two modes. + + \begin{enumerate} + + \item 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 + @{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 @{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 @{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. - \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 + \item 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. + \end{enumerate} + 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