12 subsection {* Contributions *}

    14 text {*

    15   We present the detailed lifting procedure, which was not shown before.

    16 

    17   The quotient package presented in this paper has the following

    18   advantages over existing packages:

    19   \begin{itemize}

    20 

    21   \item We define quotient composition, function map composition and

    22     relation map composition. This lets lifting polymorphic types with

    23     subtypes quotiented as well. We extend the notions of

    24     respectfullness and preservation to cope with quotient

    25     composition.

    26 

    27   \item We allow lifting only some occurrences of quotiented

    28     types. Rsp/Prs extended. (used in nominal)

    29 

    30   \item We regularize more thanks to new lemmas. (inductions in

    31     nominal).

    32 

    33   \item The quotient package is very modular. Definitions can be added

    34     separately, rsp and prs can be proved separately and theorems can

    35     be lifted on a need basis. (useful with type-classes).

    36 

    37   \item Can be used both manually (attribute, separate tactics,

    38     rsp/prs databases) and programatically (automated definition of

    39     lifted constants, the rsp proof obligations and theorem statement

    40     translation according to given quotients).

    41 

    42   \end{itemize}

    43 *}

    44 

    45 section {* Quotient Type*}

    46 

    47 text {*

    48   Defintion of quotient,

    49 

    50   Equivalence,

    51 

    52   Relation map and function map

    53 *}

    54 

    55 section {* Constants *}

    56 

    57 text {*

    58   Rep and Abs, Rsp and Prs

    59 *}

    60 

    61 section {* Lifting Theorems *}

    62 

    63 section {* Related Work *}

    64 

    65 text {*

    66   \begin{itemize}

    67 

    68   \item Peter Homeier's package (and related work from there), John

    69     Harrison's one.

    70 

    71   \item Manually defined quotients in Isabelle/HOL Library (Larry's

    72     quotients, Markus's Quotient\_Type, Dixon's FSet, \ldots)

    73 

    74   \item Oscar Slotosch defines quotient-type automatically but no

    75     lifting.

    76 

    77   \item PER. And how to avoid it.

    78 

    79   \item Necessity of Hilbert Choice op.

    80 

    81   \item Setoids in Coq

    82 

    83   \end{itemize}

    84 *}