--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Feb 14 11:16:07 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Feb 14 12:40:55 2012 +0100
@@ -1261,6 +1261,19 @@
@{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_thm"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "quot_lifted"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "quot_respect"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "quot_preserve"} & : & @{text attribute} \\
\end{matharray}
The quotient package defines a new quotient type given a raw type
@@ -1280,16 +1293,30 @@
@{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
+
+ \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.
@@ -1301,6 +1328,65 @@
\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.
+
+ \item @{attribute (HOL) quot_thm} declares that a certain theorem
+ is a quotient extension theorem. Quotient extension theorems
+ allow for quotienting inside container types. Given a polymorphic
+ type that serves as a container, a map function defined for this
+ container using @{command (HOL) "enriched_type"} and a relation
+ map defined for for the container type, the quotient extension
+ theorem should be @{term "Quotient R Abs Rep \<Longrightarrow> Quotient
+ (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems
+ are stored in a database and are used all the steps of lifting
+ theorems.
+
\end{description}
*}