(*<*)+ −
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+ −
(*>*)+ −