--- 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 \<rightarrow> local_theory"}\\
+ @{command_def (HOL) "lift_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
+ @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\
+ @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
+ @{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 :: \<tau> is t"}
+ Defines a new function @{text f} with an abstract type @{text \<tau>} 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 \<rightarrow> proof(prove)"}\\
@{command_def (HOL) "quotient_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
- @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\
- @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
+ @{command_def (HOL) "print_quotmapsQ3"} & : & @{text "context \<rightarrow>"}\\
+ @{command_def (HOL) "print_quotientsQ3"} & : & @{text "context \<rightarrow>"}\\
@{command_def (HOL) "print_quotconsts"} & : & @{text "context \<rightarrow>"}\\
@{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.
--- 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.