# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272528993 -7200
# Node ID a3adeb5d596b1e46375d778182e299529ebd7e01
# Parent  760257a66604874fa2c5a08049ad63507e57af41# Parent  8feedc0d4ea837d015c45669ecfd18706a1af081
merged

diff -r 760257a66604 -r a3adeb5d596b Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu Apr 29 10:16:15 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Thu Apr 29 10:16:33 2010 +0200
@@ -9,8 +9,80 @@
 
 text {* TBD *}
 
+subsection {* Contributions *}
 
+text {*
+  We present the detailed lifting procedure, which was not shown before.
+
+  The quotient package presented in this paper has the following
+  advantages over existing packages:
+  \begin{itemize}
+
+  \item We define quotient composition, function map composition and
+    relation map composition. This lets lifting polymorphic types with
+    subtypes quotiented as well. We extend the notions of
+    respectfullness and preservation to cope with quotient
+    composition.
+
+  \item We allow lifting only some occurrences of quotiented
+    types. Rsp/Prs extended. (used in nominal)
+
+  \item We regularize more thanks to new lemmas. (inductions in
+    nominal).
+
+  \item The quotient package is very modular. Definitions can be added
+    separately, rsp and prs can be proved separately and theorems can
+    be lifted on a need basis. (useful with type-classes).
+
+  \item Can be used both manually (attribute, separate tactics,
+    rsp/prs databases) and programatically (automated definition of
+    lifted constants, the rsp proof obligations and theorem statement
+    translation according to given quotients).
+
+  \end{itemize}
+*}
+
+section {* Quotient Type*}
+
+text {*
+  Defintion of quotient,
+
+  Equivalence,
+
+  Relation map and function map
+*}
+
+section {* Constants *}
+
+text {*
+  Rep and Abs, Rsp and Prs
+*}
+
+section {* Lifting Theorems *}
+
+section {* Related Work *}
+
+text {*
+  \begin{itemize}
+
+  \item Peter Homeier's package (and related work from there), John
+    Harrison's one.
+
+  \item Manually defined quotients in Isabelle/HOL Library (Larry's
+    quotients, Markus's Quotient\_Type, Dixon's FSet, \ldots)
+
+  \item Oscar Slotosch defines quotient-type automatically but no
+    lifting.
+
+  \item PER. And how to avoid it.
+
+  \item Necessity of Hilbert Choice op.
+
+  \item Setoids in Coq
+
+  \end{itemize}
+*}
 
 (*<*)
 end
-(*>*)
\ No newline at end of file
+(*>*)