(*<*)+ −
theory Paper+ −
imports "Quotient"+ −
"LaTeXsugar"+ −
begin+ −
+ −
notation (latex output)+ −
rel_conj ("_ OOO _" [53, 53] 52)+ −
and+ −
fun_map ("_ ---> _" [51, 51] 50)+ −
and+ −
fun_rel ("_ ===> _" [51, 51] 50)+ −
+ −
ML {*+ −
fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;+ −
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>+ −
let+ −
val concl =+ −
Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)+ −
in+ −
case concl of (_ $ l $ r) => proj (l, r)+ −
| _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)+ −
end);+ −
*}+ −
setup {*+ −
Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>+ −
Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>+ −
Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))+ −
*}+ −
(*>*)+ −
+ −
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+ −
+ −
% I would avoid substraction for natural numbers.+ −
+ −
@{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"}:+ −
+ −
@{thm concat.simps(1)}\\+ −
@{thm concat.simps(2)[no_vars]}+ −
+ −
\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 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 {*+ −
In this section we present the definitions of a quotient that follow+ −
those by Homeier, the proofs can be found there.+ −
+ −
\begin{definition}[Quotient]+ −
A relation $R$ with an abstraction function $Abs$+ −
and a representation function $Rep$ is a \emph{quotient}+ −
if and only if:+ −
+ −
\begin{enumerate}+ −
\item @{thm (rhs1) Quotient_def[of "R", no_vars]}+ −
\item @{thm (rhs2) Quotient_def[of "R", no_vars]}+ −
\item @{thm (rhs3) Quotient_def[of "R", no_vars]}+ −
\end{enumerate}+ −
+ −
\end{definition}+ −
+ −
\begin{definition}[Relation map and function map]+ −
@{thm fun_rel_def[no_vars]}\\+ −
@{thm fun_map_def[no_vars]}+ −
\end{definition}+ −
+ −
The main theorems for building higher order quotients is:+ −
\begin{lemma}[Function Quotient]+ −
If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]}+ −
then @{thm (concl) fun_quotient[no_vars]}+ −
\end{lemma}+ −
+ −
*}+ −
+ −
section {* Constants *}+ −
+ −
(* Describe what containers are? *)+ −
+ −
text {*+ −
\begin{definition}[Composition of Relations]+ −
@{abbrev "rel_conj R1 R2"}+ −
\end{definition}+ −
+ −
The first operation that we describe is the generation of+ −
aggregate Abs or Rep function for two given compound types.+ −
This operation will be used for the constant defnitions+ −
and for the translation of theorems statements. It relies on+ −
knowing map functions and relation functions for container types.+ −
It follows the following algorithm:+ −
+ −
\begin{itemize}+ −
\item For equal types or free type variables return identity.+ −
+ −
\item For function types recurse, change the Rep/Abs flag to+ −
the opposite one for the domain type and compose the+ −
results with @{term "fun_map"}.+ −
+ −
\item For equal type constructors use the appropriate map function+ −
applied to the results for the arguments.+ −
+ −
\item For unequal type constructors are unequal, we look in the+ −
quotients information for a raw type quotient type pair that+ −
matches the given types. We apply the environment to the arguments+ −
and recurse composing it with the aggregate map function.+ −
\end{itemize}+ −
+ −
+ −
+ −
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$).+ −
+ −
Separtion of regularization from injection thanks to the following 2 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~\cite{Homeier05} (and related work from there)+ −
\item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems+ −
but only first order.+ −
+ −
\item PVS~\cite{PVS:Interpretations}+ −
\item MetaPRL~\cite{Nogin02}+ −
\item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type,+ −
Dixon's FSet, \ldots)+ −
+ −
\item Oscar Slotosch defines quotient-type automatically but no+ −
lifting~\cite{Slotosch97}.+ −
+ −
\item PER. And how to avoid it.+ −
+ −
\item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06}+ −
+ −
\item Setoids in Coq and \cite{ChicliPS02}+ −
+ −
\end{itemize}+ −
*}+ −
+ −
(*<*)+ −
end+ −
(*>*)+ −