(*<*)+
−
theory Paper+
−
imports "Quotient" +
−
        "LaTeXsugar"+
−
begin+
−
+
−
notation (latex output)+
−
  fun_rel ("_ ===> _" [51, 51] 50)+
−
+
−
(*>*)+
−
+
−
section {* Introduction *}+
−
+
−
text {* +
−
  {\hfill quote by Larry}\bigskip+
−
+
−
  \noindent+
−
  Isabelle is a generic theorem prover in which many logics can be implemented. +
−
  The most widely used one, however, is+
−
  Higher-Order Logic (HOL). This logic consists of a small number of +
−
  axioms and inference+
−
  rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted +
−
  mechanisms for extending the logic: one is the definition of new constants+
−
  in terms of existing ones; the other is the introduction of new types+
−
  by identifying non-empty subsets in existing types. It is well understood +
−
  to use both mechanism for dealing with quotient constructions in HOL (cite Larry).+
−
  For example the integers in Isabelle/HOL are constructed by a quotient construction over +
−
  the type @{typ "nat \<times> nat"} and the equivalence relation+
−
+
−
  @{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"}+
−
+
−
  \noindent+
−
  Similarly one can construct the type of finite sets by quotienting lists+
−
  according to the equivalence relation+
−
+
−
  @{text [display] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}+
−
+
−
  \noindent+
−
  where @{text "\<in>"} stands for membership in a list.+
−
+
−
  The problem is that in order to start reasoning about, for example integers, +
−
  definitions and theorems need to be transferred, or \emph{lifted}, +
−
  from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}. +
−
  This lifting usually requires a lot of tedious reasoning effort.+
−
  The purpose of a \emph{quotient package} is to ease the lifting and automate+
−
  the reasoning involved as much as possible. Such a package is a central+
−
  component of the new version of Nominal Isabelle where representations +
−
  of alpha-equated terms are constructed according to specifications given by+
−
  the user. +
−
  +
−
  In the context of HOL, there have been several quotient packages (...). The+
−
  most notable is the one by Homeier (...) implemented in HOL4. However, what is+
−
  surprising, none of them can deal compositions of quotients, for example with +
−
  lifting theorems about @{text "concat"}:+
−
+
−
  @{text [display] "concat definition"}+
−
  +
−
  \noindent+
−
  One would like to lift this definition to the operation+
−
  +
−
  @{text [display] "union definition"}+
−
+
−
  \noindent+
−
  What is special about this operation is that we have as input+
−
  lists of lists which after lifting turn into finite sets of finite+
−
  sets. +
−
*}+
−
+
−
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+
−
(*>*)+
−