(*<*)+
−
theory Paper+
−
imports "Quotient" +
−
        "LaTeXsugar"+
−
begin+
−
(*>*)+
−
+
−
section {* Introduction *}+
−
+
−
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+
−
(*>*)+
−