# HG changeset patch # User Cezary Kaliszyk # Date 1332758163 -7200 # Node ID de3a893631433b8617a1fb00c16d48afa095665c # Parent d003938cc9521afacd58b78bcc559c2630d143c3 qpaper-jv add a section about descending etc diff -r d003938cc952 -r de3a89363143 Quotient-Paper-jv/Paper.thy --- a/Quotient-Paper-jv/Paper.thy Wed Mar 21 20:34:04 2012 +0000 +++ b/Quotient-Paper-jv/Paper.thy Mon Mar 26 12:36:03 2012 +0200 @@ -283,6 +283,8 @@ {\bf EXAMPLE BY HUFFMAN @{thm map_concat_fset}} +%%%TODO Update the contents. + In addition we are able to clearly specify what is involved in the lifting process (this was only hinted at in \cite{Homeier05} and implemented as a ``rough recipe'' in ML-code). A pleasing side-result @@ -914,6 +916,8 @@ %%% discussions about the generality and limitation of the approach %%% proposed there +%%% TODO: This introduction is same as the introduction to the previous section. + \noindent The main benefit of a quotient package is to lift automatically theorems over raw types to theorems over quotient types. We will perform this lifting in @@ -946,11 +950,12 @@ \noindent which means, stringed together, the raw theorem implies the quotient theorem. - In contrast to other quotient packages, our package requires that the user specifies - both, the @{text "raw_thm"} (as theorem) and the \emph{term} of the @{text "quot_thm"}.\footnote{Though we - also provide a fully automated mode, where the @{text "quot_thm"} is guessed - from the form of @{text "raw_thm"}.} As a result, the user has fine control - over which parts of a raw theorem should be lifted. + The core of the quotient package requires both the @{text "raw_thm"} (as a + theorem) and the \emph{term} of the @{text "quot_thm"}. This lets the user + have a finer control over which parts of a raw theorem should be lifted. + We also provide more automated modes where either the @{text "quot_thm"} + is guessed from the form of @{text "raw_thm"} or the @{text "raw_thm"} is + guessed from the current goal and these are described in Section \ref{sec:descending}. The second and third proof step performed in package will always succeed if the appropriate respectfulness and preservation theorems are given. In contrast, the first @@ -1156,6 +1161,127 @@ %in two equal terms that can be solved by reflexivity. *} +section {* Derivation of the shape of lifted and raw theorems\label{sec:descending} *} + +text {* + In the previous sections we have assumed, that the user specifies + both the raw theorem and the statement of the quotient one. + This allows complete flexibility, as to which parts of the statement + are lifted to the quotient level and which are intact. In + other implementations of automatic quotients (for example Homeier's + package) only the raw theorem is given to the quotient package and + the package is able to guess the quotient one. In this + section we give examples where there are multiple possible valid lifted + theorems starting from a raw one. We also show a heuristic for + computing the quotient theorem from a raw one, and a mechanism for + guessing a raw theorem starting with a quotient one. +*} + +subsection {* Multiple lifted theorems *} + +text {* + There are multiple reasons why multiple valid lifted theorems can arize. + Below we describe three possible scenarios: multiple raw variable, + multiple quotients for the same raw type and multiple quotients. + + Given a raw theorem there are often several variables that include + a raw type. It this case, one can choose which of the variables to + lift. In certain cases this can lead to a number of valid theorem + statements, however type constraints may disallow certain combinations. + Lets see an example where multiple variables can have different types. + The Isabelle/HOL induction principle for two lists is: + \begin{isabelle}\ \ \ \ \ %%% + @{thm list_induct2'} + \end{isabelle} + + the conclusion is a predicate of the form @{text "P xs ys"}, where + the two variables are lists. When lifting such theorem to the quotient + type one can choose if one want to quotient @{text "xs"} or @{text "ys"}, or + both. All these give rise to valid quotiented theorems, however the + automatic mode (or other quotient packages) would derive only the version + with both being quotiented, namely: + \begin{isabelle}\ \ \ \ \ %%% + @{thm list_induct2'[quot_lifted]} + \end{isabelle} + + A second scenario, where multiple possible quotient theorems arise is + when a single raw type is used in two quotients. Consider three quotients + of the list type: finite sets, finite multisets and lists with distinct + elements. We have developed all three types with the help of the quotient + package. Given a theorem that talks about lists --- for example the regular + induction principle --- one can lift it to three possible theorems: the + induction principle for finite sets, induction principle for finite + multisets or the induction principle for distinct lists. Again given an + induction principle for two lists this gives rise to 15 possible valid + lifted theorems. + + In our developments using the quotient package we also encountered a + scenario where multiple valid theorem statements arise, but the raw + types are not identical. Consider the type of lambda terms, where the + variables are indexed with strings. Quotienting lambda terms by alpha + equivalence gives rise to a Nominal construction~\cite{Nominal}. However + at the same time the type of strings being a list of characters can + lift to theorems about finite sets of characters. +*} + +subsection {* Derivation of the shape of theorems *} + +text {* + To derive a the shape of a lifted or raw theorem the quotient package + first builds a type and term substitution. + + The list of type substitution is created by taking the pairs + @{text "(raw_type, quotient_type)"} for every user defined quotient. + The term substitutions are of two types: First for every user-defined + quotient constant, the pair @{text "(raw_term, quotient_constant)"} + is included in the substitution. Second, for every quotient relation + @{text "\"} the pair @{text "(\, =)"} with the equality being the + equality on the defined quotient type is included in the substitution. + + The derivation function next traverses the theorem statement expressed + as a term and replaces the types of all free variables and of all + lambda-abstractions using the type substitution. For every constant + is not matched by the term substitution and we perform the type substitution + on the type of the constant (this is necessary for quotienting theorems + with polymorphic constants) or the type of the substitution is matched + and the match is returned. + + The heuristic defined above is greedy and according to our experience + this is what the user wants. The procedure may in some cases produce + theorem statements that do not type-check. However verifying all + possible theorem statements is too costly in general. +*} + +subsection {* Interaction modes and derivation of the the shape of theorems *} + +text {* + In the quotient package we provide three interaction modes, that use + can the procedure procedure defined in the previous subsection. + + First, the completely manual mode which we implemented as the + Isabelle method @{text lifting}. In this mode the user first + proves the raw theorem. Then the lifted theorem can be proved + by the method lifting, that takes the reference to the raw theorem + (or theorem list) as an argument. Such completely manual mode is + necessary for theorems where the specification of the lifted theorem + from the raw one is not unique, which we discussed in the previous + subsection. + + Next, we provide a mode for automatically lifting a given + raw theorem. We implemented this mode as an isabelle attribute, + so given the raw theorem @{text thm}, the user can refer to the + theorem @{text "thm[quot_lifted]"}. + + Finally we provie a method for translating a given quotient + level theorem to a raw one. We implemented this as an Isabelle + method @{text descending}. The user starts with expressing a + quotient level theorem statement and applies this method. + The quotient package derives a raw level statement and assumes + it as a subgoal. Given that this subgoal is proved, the quotient + package can lift the raw theorem fulfilling the proof of the + original lifted theorem statement. +*} + section {* Conclusion and Related Work\label{sec:conc}*} text {* @@ -1220,7 +1346,10 @@ {\bf Acknowledgements:} We would like to thank Peter Homeier for the many discussions about his HOL4 quotient package and explaining to us some of its finer points in the implementation. Without his patient - help, this work would have been impossible. + help, this work would have been impossible. We would like to thank + Andreas Lochbiler for his comments on the first version of the quotient + package, in particular for the suggestions about the descending method. + *} text_raw {* @@ -1333,7 +1462,6 @@ - Show the proof as much simpler than Homeier's one \item ??? Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp) \item Lifting vs Descending vs quot\_lifted - - Mention Andreas Lochbiler in Acknowledgements - automatic theorem translation heuristic \item Partial equivalence quotients - Bounded abstraction