diff -r 578e0265b235 -r 9e7047159f43 Quotient-Paper-jv/Paper.thy
--- a/Quotient-Paper-jv/Paper.thy	Thu Dec 22 13:10:30 2011 +0000
+++ b/Quotient-Paper-jv/Paper.thy	Thu Dec 22 13:10:58 2011 +0000
@@ -128,10 +128,14 @@
   "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
   natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
   such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in
-  terms of operations on pairs of natural numbers (namely @{text
-  "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
-  m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).
-  Similarly one can construct %%the type of
+  terms of operations on pairs of natural numbers:
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2, m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}
+  \end{isabelle}
+
+  \noindent
+  Similarly one can construct the type of
   finite sets, written @{term "\<alpha> fset"},
   by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
 
@@ -165,6 +169,9 @@
   makes the formal
   proof of the substitution lemma almost trivial.
 
+  {\bf MAYBE AN EAMPLE FOR PARTIAL QUOTIENTS?}
+
+
   The difficulty is that in order to be able to reason about integers, finite
   sets or $\alpha$-equated lambda-terms one needs to establish a reasoning
   infrastructure by transferring, or \emph{lifting}, definitions and theorems
@@ -318,20 +325,22 @@
   of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
   from Homeier \cite{Homeier05}.
 
+  {\bf EXAMPLE BY HUFFMAN ABOUT @{thm map_concat}}
+
   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
   is that our procedure for lifting theorems is completely deterministic
   following the structure of the theorem being lifted and the theorem
-  on the quotient level. Space constraints, unfortunately, allow us to only
+  on the quotient level. {\it Space constraints, unfortunately, allow us to only
   sketch this part of our work in Section 5 and we defer the reader to a longer
-  version for the details. However, we will give in Section 3 and 4 all
+  version for the details.} However, we will give in Section 3 and 4 all
   definitions that specify the input and output data of our three-step
   lifting procedure. Appendix A gives an example how our quotient
   package works in practise.
 *}
 
-section {* Preliminaries and General\\ Quotients\label{sec:prelims} *}
+section {* Preliminaries and General Quotients\label{sec:prelims} *}
 
 text {*
   \noindent
@@ -498,7 +507,7 @@
   \end{isabelle}
 *}
 
-section {* Quotient Types and Quotient\\ Definitions\label{sec:type} *}
+section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 
 text {*
   \noindent
@@ -758,7 +767,7 @@
   \end{proof}
 *}
 
-section {* Respectfulness and\\ Preservation \label{sec:resp} *}
+section {* Respectfulness and Preservation \label{sec:resp} *}
 
 text {*
   \noindent
@@ -1210,6 +1219,7 @@
   \cite{BengtsonParow09} and a strong normalisation result for cut-elimination
   in classical logic \cite{UrbanZhu08}.
 
+  {\bf INSTEAD OF NOMINAL WORK, GIVE WORK BY BULWAHN ET AL?}
 
   There is a wide range of existing literature for dealing with quotients
   in theorem provers.  Slotosch~\cite{Slotosch97} implemented a mechanism that
@@ -1355,6 +1365,27 @@
   where @{text x} is of type integer.
   Although seemingly simple, arriving at this result without the help of a quotient
   package requires a substantial reasoning effort (see \cite{Paulson06}).
+
+  {\bf \begin{itemize}
+  \item Type maps and Relation maps (show the case for functions)
+  \item Quotient extensions
+  \item Respectfulness and preservation
+  - Show special cases for quantifiers and lambda
+  \item Quotient-type locale
+  - 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
+  - automatic theorem translation heuristic
+  \item Partial equivalence quotients
+  - Bounded abstraction
+  - Respects
+  - partial descending
+  \item The heuristics for automatic regularization, injection and cleaning.
+  \item A complete example of a lifted theorem together with the regularized
+  injected and cleaned statement
+  \item Examples of quotients and properties that we used the package for.
+  \item co/contra-variance from Ondrej should be taken into account
+  \end{itemize}}
 *}