# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1324530937 0
# Node ID 8bad9887ad902930f5846c9bbea4e145c24627e4
# Parent  06950f2b4443bd131852efdb502c4ade20e328ca
moved TODO into the paper

diff -r 06950f2b4443 -r 8bad9887ad90 Quotient-Paper-jv/Paper.thy
--- a/Quotient-Paper-jv/Paper.thy	Thu Dec 22 04:47:05 2011 +0000
+++ b/Quotient-Paper-jv/Paper.thy	Thu Dec 22 05:15:37 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
 
@@ -321,14 +325,16 @@
   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.
@@ -1213,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
@@ -1358,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}}
 *}