(*<*)+
−
theory Paper+
−
imports "Quotient" +
−
        "LaTeXsugar"+
−
begin+
−
+
−
notation (latex output)+
−
  fun_rel ("_ ===> _" [51, 51] 50)+
−
+
−
(*>*)+
−
+
−
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 *}+
−
+
−
text {* TBD *}+
−
+
−
text {* Why providing a statement to prove is necessary is some cases *}+
−
+
−
subsection {* Regularization *}+
−
+
−
text {*+
−
Transformation of the theorem statement:+
−
\begin{itemize}+
−
\item Quantifiers and abstractions involving raw types replaced by bounded ones.+
−
\item Equalities involving raw types replaced by bounded ones.+
−
\end{itemize}+
−
+
−
The procedure.+
−
+
−
Example of non-regularizable theorem ($0 = 1$).+
−
+
−
New regularization lemmas:+
−
\begin{lemma}+
−
If @{term R2} is an equivalence relation, then:+
−
\begin{eqnarray}+
−
@{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\+
−
@{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}+
−
\end{eqnarray}+
−
\end{lemma}+
−
+
−
*}+
−
+
−
subsection {* Injection *}+
−
+
−
subsection {* Cleaning *}+
−
+
−
text {* Preservation of quantifiers, abstractions, relations, quotient-constants+
−
  (definitions) and user given constant preservation lemmas *}+
−
+
−
section {* Examples *}+
−
+
−
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+
−
(*>*)+
−