# HG changeset patch # User kuncar # Date 1335539196 -7200 # Node ID f6cf7148d45284443979de9eb23139439b013919 # Parent 4ad62c5f9f88b963219d324eca0fdfcf4ae79728 documentation for the Lifting package in Isar-ref diff -r 4ad62c5f9f88 -r f6cf7148d452 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Apr 27 15:24:37 2012 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Apr 27 17:06:36 2012 +0200 @@ -1254,14 +1254,99 @@ \end{description} *} +section {* Lifting package *} + +text {* + \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) "print_quotmaps"} & : & @{text "context \"}\\ + @{command_def (HOL) "print_quotients"} & : & @{text "context \"}\\ + @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\ + @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\ + \end{matharray} + + @{rail " + @@{command (HOL) setup_lifting} ('(' 'no_abs_code' ')')? \\ + @{syntax thmref} @{syntax thmref}?; + "} + + @{rail " + @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \\ + 'is' @{syntax term}; + "} + + \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_abs_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 registred as abstract code equations. + + \item @{command (HOL) "lift_definition"} @{text "f :: \ is 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 + 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 package. + + Integration with code_abstype: For typedefs (e.g. subtypes + corresponding to a datatype invariant, such as dlist), + @{command (HOL) "lift_definition"} + generates a code certificate theorem @{text f.rep_eq} and sets up + code generation for each constant. + + \item @{command (HOL) "print_quotmaps"} prints stored quotient map + theorems. + + \item @{command (HOL) "print_quotients"} prints stored quotient 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. + + \item @{attribute (HOL) invariant_commute} registers a theorem which shows a relationship + between the constant @{text Lifting.invariant} (used for internal encoding of proper subtypes) + 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. + + + \end{description} + +*} + section {* Quotient types *} text {* \begin{matharray}{rcl} @{command_def (HOL) "quotient_type"} & : & @{text "local_theory \ proof(prove)"}\\ @{command_def (HOL) "quotient_definition"} & : & @{text "local_theory \ proof(prove)"}\\ - @{command_def (HOL) "print_quotmaps"} & : & @{text "context \"}\\ - @{command_def (HOL) "print_quotients"} & : & @{text "context \"}\\ + @{command_def (HOL) "print_quotmapsQ3"} & : & @{text "context \"}\\ + @{command_def (HOL) "print_quotientsQ3"} & : & @{text "context \"}\\ @{command_def (HOL) "print_quotconsts"} & : & @{text "context \"}\\ @{method_def (HOL) "lifting"} & : & @{text method} \\ @{method_def (HOL) "lifting_setup"} & : & @{text method} \\ @@ -1323,10 +1408,10 @@ \item @{command (HOL) "quotient_definition"} defines a constant on the quotient type. - \item @{command (HOL) "print_quotmaps"} prints quotient map + \item @{command (HOL) "print_quotmapsQ3"} prints quotient map functions. - \item @{command (HOL) "print_quotients"} prints quotients. + \item @{command (HOL) "print_quotientsQ3"} prints quotients. \item @{command (HOL) "print_quotconsts"} prints quotient constants. diff -r 4ad62c5f9f88 -r f6cf7148d452 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Apr 27 15:24:37 2012 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Apr 27 17:06:36 2012 +0200 @@ -1774,6 +1774,119 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsection{Lifting package% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{HOL}{command}{setup\_lifting}\hypertarget{command.HOL.setup-lifting}{\hyperlink{command.HOL.setup-lifting}{\mbox{\isa{\isacommand{setup{\isaliteral{5F}{\isacharunderscore}}lifting}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}}\\ + \indexdef{HOL}{command}{lift\_definition}\hypertarget{command.HOL.lift-definition}{\hyperlink{command.HOL.lift-definition}{\mbox{\isa{\isacommand{lift{\isaliteral{5F}{\isacharunderscore}}definition}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ + \indexdef{HOL}{command}{print\_quotmaps}\hypertarget{command.HOL.print-quotmaps}{\hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ + \indexdef{HOL}{command}{print\_quotients}\hypertarget{command.HOL.print-quotients}{\hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ + \indexdef{HOL}{attribute}{quot\_map}\hypertarget{attribute.HOL.quot-map}{\hyperlink{attribute.HOL.quot-map}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}map}}}} & : & \isa{attribute} \\ + \indexdef{HOL}{attribute}{invariant\_commute}\hypertarget{attribute.HOL.invariant-commute}{\hyperlink{attribute.HOL.invariant-commute}{\mbox{\isa{invariant{\isaliteral{5F}{\isacharunderscore}}commute}}}} & : & \isa{attribute} \\ + \end{matharray} + + \begin{railoutput} +\rail@begin{5}{} +\rail@term{\hyperlink{command.HOL.setup-lifting}{\mbox{\isa{\isacommand{setup{\isaliteral{5F}{\isacharunderscore}}lifting}}}}}[] +\rail@bar +\rail@nextbar{1} +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] +\rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}abs{\isaliteral{5F}{\isacharunderscore}}code}}[] +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] +\rail@endbar +\rail@cr{3} +\rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[] +\rail@bar +\rail@nextbar{4} +\rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[] +\rail@endbar +\rail@end +\end{railoutput} + + + \begin{railoutput} +\rail@begin{4}{} +\rail@term{\hyperlink{command.HOL.lift-definition}{\mbox{\isa{\isacommand{lift{\isaliteral{5F}{\isacharunderscore}}definition}}}}}[] +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[] +\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[] +\rail@bar +\rail@nextbar{1} +\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[] +\rail@endbar +\rail@cr{3} +\rail@term{\isa{is}}[] +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] +\rail@end +\end{railoutput} + + + \begin{description} + + \item \hyperlink{command.HOL.setup-lifting}{\mbox{\isa{\isacommand{setup{\isaliteral{5F}{\isacharunderscore}}lifting}}}} Sets up the Lifting package to work with + a user-defined type. The user must provide either a quotient + theorem \isa{{\isaliteral{22}{\isachardoublequote}}Quotient\ R\ Abs\ Rep\ T{\isaliteral{22}{\isachardoublequote}}} or a type_definition theorem + \isa{{\isaliteral{22}{\isachardoublequote}}type{\isaliteral{5F}{\isacharunderscore}}definition\ Rep\ Abs\ A{\isaliteral{22}{\isachardoublequote}}}. + The package configures + transfer rules for equality and quantifiers on the type, and sets + up the \indexdef{HOL}{command}{lift\_definition}\hypertarget{command.HOL.lift-definition}{\hyperlink{command.HOL.lift-definition}{\mbox{\isa{\isacommand{lift{\isaliteral{5F}{\isacharunderscore}}definition}}}}} command to work with the type. + In the case of a quotient theorem, + an optional theorem \isa{{\isaliteral{22}{\isachardoublequote}}reflp\ R{\isaliteral{22}{\isachardoublequote}}} can be provided as a second argument. + This allows the package to generate stronger transfer rules. + + \hyperlink{command.HOL.setup-lifting}{\mbox{\isa{\isacommand{setup{\isaliteral{5F}{\isacharunderscore}}lifting}}}} is called automatically if a quotient type + is defined by the command \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} from the Quotient package. + + If \hyperlink{command.HOL.setup-lifting}{\mbox{\isa{\isacommand{setup{\isaliteral{5F}{\isacharunderscore}}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 \hyperlink{command.HOL.lift-definition}{\mbox{\isa{\isacommand{lift{\isaliteral{5F}{\isacharunderscore}}definition}}}} to register + (generated) code certificate theorems as abstract code equations in the code generator. + The option \isa{{\isaliteral{22}{\isachardoublequote}}no{\isaliteral{5F}{\isacharunderscore}}abs{\isaliteral{5F}{\isacharunderscore}}code{\isaliteral{22}{\isachardoublequote}}} of the command \hyperlink{command.HOL.setup-lifting}{\mbox{\isa{\isacommand{setup{\isaliteral{5F}{\isacharunderscore}}lifting}}}} + can turn off that behavior and causes that code certificate theorems generated + by \hyperlink{command.HOL.lift-definition}{\mbox{\isa{\isacommand{lift{\isaliteral{5F}{\isacharunderscore}}definition}}}} are not registred as abstract code equations. + + \item \hyperlink{command.HOL.lift-definition}{\mbox{\isa{\isacommand{lift{\isaliteral{5F}{\isacharunderscore}}definition}}}} \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ is\ t{\isaliteral{22}{\isachardoublequote}}} + Defines a new function \isa{f} with an abstract type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} in + terms of a corresponding operation \isa{t} on a representation type. + The term \isa{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 \isa{UNIV}, + the proof is discharged automatically. The obligation is + presented in a user-friendly, readable form. A respectfulness + theorem in the standard format \isa{f{\isaliteral{2E}{\isachardot}}rsp} and a transfer rule \isa{f{\isaliteral{2E}{\isachardot}}tranfer} + for the Transfer package are generated by the package. + + Integration with code_abstype: For typedefs (e.g. subtypes + corresponding to a datatype invariant, such as dlist), + \hyperlink{command.HOL.lift-definition}{\mbox{\isa{\isacommand{lift{\isaliteral{5F}{\isacharunderscore}}definition}}}} + generates a code certificate theorem \isa{f{\isaliteral{2E}{\isachardot}}rep{\isaliteral{5F}{\isacharunderscore}}eq} and sets up + code generation for each constant. + + \item \hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}} prints stored quotient map + theorems. + + \item \hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}} prints stored quotient theorems. + + \item \hyperlink{attribute.HOL.quot-map}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}map}}} registers a quotient map theorem. For examples see + \verb|~~/src/HOL/Library/Quotient_List.thy| or other Quotient_*.thy files. + + \item \hyperlink{attribute.HOL.invariant-commute}{\mbox{\isa{invariant{\isaliteral{5F}{\isacharunderscore}}commute}}} registers a theorem which shows a relationship + between the constant \isa{Lifting{\isaliteral{2E}{\isachardot}}invariant} (used for internal encoding of proper subtypes) + and a relator. + Such theorems allows the package to hide \isa{Lifting{\isaliteral{2E}{\isachardot}}invariant} from a user + in a user-readable form of a respectfulness theorem. For examples see + \verb|~~/src/HOL/Library/Quotient_List.thy| or other Quotient_*.thy files. + + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsection{Quotient types% } \isamarkuptrue% @@ -1782,8 +1895,8 @@ \begin{matharray}{rcl} \indexdef{HOL}{command}{quotient\_type}\hypertarget{command.HOL.quotient-type}{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ \indexdef{HOL}{command}{quotient\_definition}\hypertarget{command.HOL.quotient-definition}{\hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ - \indexdef{HOL}{command}{print\_quotmaps}\hypertarget{command.HOL.print-quotmaps}{\hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ - \indexdef{HOL}{command}{print\_quotients}\hypertarget{command.HOL.print-quotients}{\hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ + \indexdef{HOL}{command}{print\_quotmapsQ3}\hypertarget{command.HOL.print-quotmapsQ3}{\hyperlink{command.HOL.print-quotmapsQ3}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmapsQ{\isadigit{3}}}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ + \indexdef{HOL}{command}{print\_quotientsQ3}\hypertarget{command.HOL.print-quotientsQ3}{\hyperlink{command.HOL.print-quotientsQ3}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotientsQ{\isadigit{3}}}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ \indexdef{HOL}{command}{print\_quotconsts}\hypertarget{command.HOL.print-quotconsts}{\hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ \indexdef{HOL}{method}{lifting}\hypertarget{method.HOL.lifting}{\hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}}} & : & \isa{method} \\ \indexdef{HOL}{method}{lifting\_setup}\hypertarget{method.HOL.lifting-setup}{\hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}}} & : & \isa{method} \\ @@ -1903,10 +2016,10 @@ \item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on the quotient type. - \item \hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}} prints quotient map + \item \hyperlink{command.HOL.print-quotmapsQ3}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmapsQ{\isadigit{3}}}}}} prints quotient map functions. - \item \hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}} prints quotients. + \item \hyperlink{command.HOL.print-quotientsQ3}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotientsQ{\isadigit{3}}}}}} prints quotients. \item \hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}} prints quotient constants.