--- 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 "\<approx>"} the pair @{text "(\<approx>, =)"} 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