--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Feb 09 16:00:04 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 10 09:02:51 2012 +0100
@@ -1263,6 +1263,18 @@
@{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\
@{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
@{command_def (HOL) "print_quotconsts"} & : & @{text "context \<rightarrow>"}\\
+ @{method_def (HOL) "lifting"} & : & @{text method} \\
+ @{method_def (HOL) "lifting_setup"} & : & @{text method} \\
+ @{method_def (HOL) "descending"} & : & @{text method} \\
+ @{method_def (HOL) "descending_setup"} & : & @{text method} \\
+ @{method_def (HOL) "partiality_descending"} & : & @{text method} \\
+ @{method_def (HOL) "partiality_descending_setup"} & : & @{text method} \\
+ @{method_def (HOL) "regularize"} & : & @{text method} \\
+ @{method_def (HOL) "injection"} & : & @{text method} \\
+ @{method_def (HOL) "cleaning"} & : & @{text method} \\
+ @{attribute_def (HOL) "quot_lifted"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "quot_respect"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "quot_preserve"} & : & @{text attribute} \\
\end{matharray}
@{rail "
@@ -1276,15 +1288,27 @@
@{rail "
@@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \\
@{syntax term} 'is' @{syntax term};
-
+
constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
"}
+ @{rail "
+ @@{method (HOL) lifting} @{syntax thmrefs}?
+ ;
+
+ @@{method (HOL) lifting_setup} @{syntax thmrefs}?
+ ;
+ "}
+
\begin{description}
-
+
\item @{command (HOL) "quotient_type"} defines quotient types. The injection from a quotient type
to a raw type is called @{text rep_t}, its inverse @{text abs_t} unless explicit @{keyword (HOL)
- "morphisms"} specification provides alternative names.
+ "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 user specifies explicitely @{text partial} in which case the obligation is @{text part_equivp}.
+ A quotient defined with @{text partial} is weaker in the sense that less things can be proved
+ automatically.
\item @{command (HOL) "quotient_definition"} defines a constant on the quotient type.
@@ -1294,6 +1318,54 @@
\item @{command (HOL) "print_quotconsts"} prints quotient constants.
+ \item @{method (HOL) "lifting"} and @{method (HOL) "lifting_setup"}
+ methods match the current goal with the given raw theorem to be
+ lifted producing three new subgoals: regularization, injection and
+ cleaning subgoals. @{method (HOL) "lifting"} tries to apply the
+ heuristics for automatically solving these three subgoals and
+ leaves only the subgoals unsolved by the heuristics to the user as
+ opposed to @{method (HOL) "lifting_setup"} which leaves the three
+ subgoals unsolved.
+
+ \item @{method (HOL) "descending"} and @{method (HOL)
+ "descending_setup"} try to guess a raw statement that would lift
+ to the current subgoal. Such statement is assumed as a new subgoal
+ and @{method (HOL) "descending"} continues in the same way as
+ @{method (HOL) "lifting"} does. @{method (HOL) "descending"} tries
+ to solve the arising regularization, injection and cleaning
+ subgoals with the analoguous method @{method (HOL)
+ "descending_setup"} which leaves the four unsolved subgoals.
+
+ \item @{method (HOL) "partiality_descending"} finds the regularized
+ theorem that would lift to the current subgoal, lifts it and
+ leaves as a subgoal. This method can be used with partial
+ equivalence quotients where the non regularized statements would
+ not be true. @{method (HOL) "partiality_descending_setup"} leaves
+ the injection and cleaning subgoals unchanged.
+
+ \item @{method (HOL) "regularize"} applies the regularization
+ heuristics to the current subgoal.
+
+ \item @{method (HOL) "injection"} applies the injection heuristics
+ to the current goal using the stored quotient respectfulness
+ theorems.
+
+ \item @{method (HOL) "cleaning"} applies the injection cleaning
+ heuristics to the current subgoal using the stored quotient
+ preservation theorems.
+
+ \item @{attribute (HOL) quot_lifted} attribute tries to
+ automatically transport the theorem to the quotient type.
+ The attribute uses all the defined quotients types and quotient
+ constants often producing undesired results or theorems that
+ cannot be lifted.
+
+ \item @{attribute (HOL) quot_respect} and @{attribute (HOL)
+ quot_preserve} attributes declare a theorem as a respectfulness
+ and preservation theorem respectively. These are stored in the
+ local theory store and used by the @{method (HOL) "injection"}
+ and @{method (HOL) "cleaning"} methods respectively.
+
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Feb 09 16:00:04 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 10 09:02:51 2012 +0100
@@ -1780,6 +1780,18 @@
\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\_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} \\
+ \indexdef{HOL}{method}{descending}\hypertarget{method.HOL.descending}{\hyperlink{method.HOL.descending}{\mbox{\isa{descending}}}} & : & \isa{method} \\
+ \indexdef{HOL}{method}{descending\_setup}\hypertarget{method.HOL.descending-setup}{\hyperlink{method.HOL.descending-setup}{\mbox{\isa{descending{\isaliteral{5F}{\isacharunderscore}}setup}}}} & : & \isa{method} \\
+ \indexdef{HOL}{method}{partiality\_descending}\hypertarget{method.HOL.partiality-descending}{\hyperlink{method.HOL.partiality-descending}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending}}}} & : & \isa{method} \\
+ \indexdef{HOL}{method}{partiality\_descending\_setup}\hypertarget{method.HOL.partiality-descending-setup}{\hyperlink{method.HOL.partiality-descending-setup}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending{\isaliteral{5F}{\isacharunderscore}}setup}}}} & : & \isa{method} \\
+ \indexdef{HOL}{method}{regularize}\hypertarget{method.HOL.regularize}{\hyperlink{method.HOL.regularize}{\mbox{\isa{regularize}}}} & : & \isa{method} \\
+ \indexdef{HOL}{method}{injection}\hypertarget{method.HOL.injection}{\hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}} & : & \isa{method} \\
+ \indexdef{HOL}{method}{cleaning}\hypertarget{method.HOL.cleaning}{\hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}}} & : & \isa{method} \\
+ \indexdef{HOL}{attribute}{quot\_lifted}\hypertarget{attribute.HOL.quot-lifted}{\hyperlink{attribute.HOL.quot-lifted}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}lifted}}}} & : & \isa{attribute} \\
+ \indexdef{HOL}{attribute}{quot\_respect}\hypertarget{attribute.HOL.quot-respect}{\hyperlink{attribute.HOL.quot-respect}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}respect}}}} & : & \isa{attribute} \\
+ \indexdef{HOL}{attribute}{quot\_preserve}\hypertarget{attribute.HOL.quot-preserve}{\hyperlink{attribute.HOL.quot-preserve}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}preserve}}}} & : & \isa{attribute} \\
\end{matharray}
\begin{railoutput}
@@ -1849,10 +1861,32 @@
\end{railoutput}
+ \begin{railoutput}
+\rail@begin{2}{}
+\rail@term{\hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@endbar
+\rail@end
+\rail@begin{2}{}
+\rail@term{\hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
+
\begin{description}
-
+
\item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types. The injection from a quotient type
- to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t}, its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names.
+ to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t}, its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names. \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} requires
+ the user to prove that the relation is an equivalence relation (predicate \isa{equivp}), unless
+ the user specifies explicitely \isa{partial} in which case the obligation is \isa{part{\isaliteral{5F}{\isacharunderscore}}equivp}.
+ A quotient defined with \isa{partial} is weaker in the sense that less things can be proved
+ automatically.
\item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on the quotient type.
@@ -1862,6 +1896,51 @@
\item \hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}} prints quotient constants.
+ \item \hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}} and \hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}}
+ methods match the current goal with the given raw theorem to be
+ lifted producing three new subgoals: regularization, injection and
+ cleaning subgoals. \hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}} tries to apply the
+ heuristics for automatically solving these three subgoals and
+ leaves only the subgoals unsolved by the heuristics to the user as
+ opposed to \hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}} which leaves the three
+ subgoals unsolved.
+
+ \item \hyperlink{method.HOL.descending}{\mbox{\isa{descending}}} and \hyperlink{method.HOL.descending-setup}{\mbox{\isa{descending{\isaliteral{5F}{\isacharunderscore}}setup}}} try to guess a raw statement that would lift
+ to the current subgoal. Such statement is assumed as a new subgoal
+ and \hyperlink{method.HOL.descending}{\mbox{\isa{descending}}} continues in the same way as
+ \hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}} does. \hyperlink{method.HOL.descending}{\mbox{\isa{descending}}} tries
+ to solve the arising regularization, injection and cleaning
+ subgoals with the analoguous method \hyperlink{method.HOL.descending-setup}{\mbox{\isa{descending{\isaliteral{5F}{\isacharunderscore}}setup}}} which leaves the four unsolved subgoals.
+
+ \item \hyperlink{method.HOL.partiality-descending}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending}}} finds the regularized
+ theorem that would lift to the current subgoal, lifts it and
+ leaves as a subgoal. This method can be used with partial
+ equivalence quotients where the non regularized statements would
+ not be true. \hyperlink{method.HOL.partiality-descending-setup}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending{\isaliteral{5F}{\isacharunderscore}}setup}}} leaves
+ the injection and cleaning subgoals unchanged.
+
+ \item \hyperlink{method.HOL.regularize}{\mbox{\isa{regularize}}} applies the regularization
+ heuristics to the current subgoal.
+
+ \item \hyperlink{method.HOL.injection}{\mbox{\isa{injection}}} applies the injection heuristics
+ to the current goal using the stored quotient respectfulness
+ theorems.
+
+ \item \hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}} applies the injection cleaning
+ heuristics to the current subgoal using the stored quotient
+ preservation theorems.
+
+ \item \hyperlink{attribute.HOL.quot-lifted}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}lifted}}} attribute tries to
+ automatically transport the theorem to the quotient type.
+ The attribute uses all the defined quotients types and quotient
+ constants often producing undesired results or theorems that
+ cannot be lifted.
+
+ \item \hyperlink{attribute.HOL.quot-respect}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}respect}}} and \hyperlink{attribute.HOL.quot-preserve}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}preserve}}} attributes declare a theorem as a respectfulness
+ and preservation theorem respectively. These are stored in the
+ local theory store and used by the \hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}
+ and \hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}} methods respectively.
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%