+ −
(*<*)+ −
theory Paper+ −
imports "Quotient"+ −
"LaTeXsugar"+ −
"../Nominal/FSet"+ −
begin+ −
+ −
notation (latex output)+ −
rel_conj ("_ OOO _" [53, 53] 52)+ −
and+ −
fun_map ("_ ---> _" [51, 51] 50)+ −
and+ −
fun_rel ("_ ===> _" [51, 51] 50)+ −
and+ −
list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *)+ −
+ −
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 [display] concat.simps(1)}+ −
@{thm [display] concat.simps(2)[no_vars]}+ −
+ −
\noindent+ −
One would like to lift this definition to the operation:+ −
+ −
@{thm [display] fconcat_empty[no_vars]}+ −
@{thm [display] fconcat_insert[no_vars]}+ −
+ −
\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+ −
respectfulness 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[of "R1" "R2", 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}+ −
+ −
*}+ −
+ −
subsection {* Higher Order Logic *}+ −
+ −
text {*+ −
+ −
Types:+ −
\begin{eqnarray}\nonumber+ −
@{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber+ −
@{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)}+ −
\end{eqnarray}+ −
+ −
Terms:+ −
\begin{eqnarray}\nonumber+ −
@{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber+ −
@{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber+ −
@{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber+ −
@{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber+ −
\end{eqnarray}+ −
+ −
*}+ −
+ −
section {* Constants *}+ −
+ −
(* Say more about containers? *)+ −
+ −
text {*+ −
+ −
To define a constant on the lifted type, an aggregate abstraction+ −
function is applied to the raw constant. Below we describe the operation+ −
that generates+ −
an aggregate @{term "Abs"} or @{term "Rep"} function given the+ −
compound raw type and the compound quotient type.+ −
This operation will also be used in translations of theorem statements+ −
and in the lifting procedure.+ −
+ −
The operation is additionally able to descend into types for which+ −
maps are known. Such maps for most common types (list, pair, sum,+ −
option, \ldots) are described in Homeier, and we assume that @{text "map"}+ −
is the function that returns a map for a given type. Then REP/ABS is defined+ −
as follows:+ −
+ −
\begin{itemize}+ −
\item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}+ −
\item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}+ −
\item @{text "ABS(\<sigma>, \<sigma>)"} = @{text "id"}+ −
\item @{text "REP(\<sigma>, \<sigma>)"} = @{text "id"}+ −
\item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"} = @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}+ −
\item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"} = @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}+ −
\item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}+ −
\item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}+ −
\item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}+ −
\item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}+ −
\end{itemize}+ −
+ −
Apart from the last 2 points the definition is same as the one implemented in+ −
in Homeier's HOL package, below is the definition of @{term fconcat}+ −
that shows the last points:+ −
+ −
@{thm fconcat_def[no_vars]}+ −
+ −
The aggregate @{term Abs} function takes a finite set of finite sets+ −
and applies @{term "map rep_fset"} composed with @{term rep_fset} to+ −
its input, obtaining a list of lists, passes the result to @{term concat}+ −
obtaining a list and applies @{term abs_fset} obtaining the composed+ −
finite set.+ −
*}+ −
+ −
subsection {* Respectfulness *}+ −
+ −
text {*+ −
+ −
A respectfulness lemma for a constant states that the equivalence+ −
class returned by this constant depends only on the equivalence+ −
classes of the arguments applied to the constant. This can be+ −
expressed in terms of an aggregate relation between the constant+ −
and itself, for example the respectfullness for @{term "append"}+ −
can be stated as:+ −
+ −
@{thm [display] append_rsp[no_vars]}+ −
+ −
\noindent+ −
Which is equivalent to:+ −
+ −
@{thm [display] append_rsp_unfolded[no_vars]}+ −
+ −
Below we show the algorithm for finding the aggregate relation.+ −
This algorithm uses+ −
the relation composition which we define as:+ −
+ −
\begin{definition}[Composition of Relations]+ −
@{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate+ −
composition @{thm pred_compI[no_vars]}+ −
\end{definition}+ −
+ −
Given an aggregate raw type and quotient type:+ −
+ −
\begin{itemize}+ −
\item For equal types or free type variables return equality+ −
+ −
\item For equal type constructors use the appropriate rel+ −
function applied to the results for the argument pairs+ −
+ −
\item For unequal type constructors, look in the quotients information+ −
for a quotient type that matches the type constructor, and instantiate+ −
the type appropriately getting back an instantiation environment. We+ −
apply the environment to the arguments and recurse composing it with+ −
the aggregate relation function.+ −
+ −
\end{itemize}+ −
+ −
Again, the the behaviour of our algorithm in the last situation is+ −
novel, so lets look at the example of respectfullness for @{term concat}.+ −
The statement as computed by the algorithm above is:+ −
+ −
@{thm [display] concat_rsp[no_vars]}+ −
+ −
\noindent+ −
By unfolding the definition of relation composition and relation map+ −
we can see the equivalent statement just using the primitive list+ −
equivalence relation:+ −
+ −
@{thm [display] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]}+ −
+ −
The statement reads that, for any lists of lists @{term a} and @{term b}+ −
if there exist intermediate lists of lists @{term "a'"} and @{term "b'"}+ −
such that each element of @{term a} is in the relation with an appropriate+ −
element of @{term a'}, @{term a'} is in relation with @{term b'} and each+ −
element of @{term b'} is in relation with the appropriate element of+ −
@{term b}.+ −
+ −
*}+ −
+ −
subsection {* Preservation *}+ −
+ −
text {*+ −
To be able to lift theorems that talk about constants that are not+ −
lifted but whose type changes when lifting is performed additionally+ −
preservation theorems are needed.+ −
+ −
To lift theorems that talk about insertion in lists of lifted types+ −
we need to know that for any quotient type with the abstraction and+ −
representation functions @{text "Abs"} and @{text Rep} we have:+ −
+ −
@{thm [display] (concl) cons_prs[no_vars]}+ −
+ −
This is not enough to lift theorems that talk about quotient compositions.+ −
For some constants (for example empty list) it is possible to show a+ −
general compositional theorem, but for @{term "op #"} it is necessary+ −
to show that it respects the particular quotient type:+ −
+ −
@{thm [display] insert_preserve2[no_vars]}+ −
*}+ −
+ −
subsection {* Composition of Quotient theorems *}+ −
+ −
text {*+ −
Given two quotients, one of which quotients a container, and the+ −
other quotients the type in the container, we can write the+ −
composition of those quotients. To compose two quotient theorems+ −
we compose the relations with relation composition+ −
and the abstraction and relation functions with function composition.+ −
The @{term "Rep"} and @{term "Abs"} functions that we obtain are+ −
the same as the ones created by in the aggregate functions and the+ −
relation is the same as the one given by aggregate relations.+ −
This becomes especially interesting+ −
when we compose the quotient with itself, as there is no simple+ −
intermediate step.+ −
+ −
Lets take again the example of @{term concat}. To be able to lift+ −
theorems that talk about it we will first prove the composition+ −
quotient theorems, which then lets us perform the lifting procedure+ −
in an unchanged way:+ −
+ −
@{thm [display] quotient_compose_list[no_vars]}+ −
*}+ −
+ −
+ −
section {* Lifting Theorems *}+ −
+ −
text {*+ −
The core of the quotient package takes an original theorem that+ −
talks about the raw types, and the statement of the theorem that+ −
it is supposed to produce. This is different from other existing+ −
quotient packages, where only the raw theorems was necessary.+ −
We notice that in some cases only some occurrences of the raw+ −
types need to be lifted. This is for example the case in the+ −
new Nominal package, where a raw datatype that talks about+ −
pairs of natural numbers or strings (being lists of characters)+ −
should not be changed to a quotient datatype with constructors+ −
taking integers or finite sets of characters. To simplify the+ −
use of the quotient package we additionally provide an automated+ −
statement translation mechanism that replaces occurrences of+ −
types that match given quotients by appropriate lifted types.+ −
+ −
Lifting the theorems is performed in three steps. In the following+ −
we call these steps \emph{regularization}, \emph{injection} and+ −
\emph{cleaning} following the names used in Homeier's HOL+ −
implementation.+ −
+ −
We first define the statement of the regularized theorem based+ −
on the original theorem and the goal theorem. Then we define+ −
the statement of the injected theorem, based on the regularized+ −
theorem and the goal. We then show the 3 proofs, and all three+ −
can be performed independently from each other.+ −
+ −
*}+ −
+ −
subsection {* Regularization and Injection statements *}+ −
+ −
text {*+ −
+ −
The function that gives the statement of the regularized theorem+ −
takes the statement of the raw theorem (a term) and the statement+ −
of the lifted theorem. The intuition behind the procedure is that+ −
it replaces quantifiers and abstractions involving raw types+ −
by bounded ones, and equalities involving raw types are replaced+ −
by appropriate aggregate relations. It is defined as follows:+ −
+ −
\begin{itemize}+ −
\item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}+ −
\item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}+ −
\item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}+ −
\item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}+ −
\item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}+ −
\item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}+ −
\item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}+ −
\item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}+ −
\item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}+ −
\end{itemize}+ −
+ −
Existential quantifiers and unique existential quantifiers are defined+ −
similarily to the universal one.+ −
+ −
The function that gives the statment of the injected theorem+ −
takes the statement of the regularized theorems and the statement+ −
of the lifted theorem both as terms.+ −
+ −
\begin{itemize}+ −
\item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}+ −
\item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}+ −
\item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}+ −
\item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"}+ −
\item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"}+ −
\item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}+ −
\item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"}+ −
\item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}+ −
\item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"}+ −
\item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}+ −
\end{itemize}+ −
+ −
For existential quantifiers and unique existential quantifiers it is+ −
defined similarily to the universal one.+ −
+ −
*}+ −
+ −
subsection {* Proof of Regularization *}+ −
+ −
text {*+ −
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}+ −
+ −
Other lemmas used in regularization:+ −
@{thm [display] ball_reg_eqv[no_vars]}+ −
@{thm [display] bex_reg_eqv[no_vars]}+ −
@{thm [display] babs_reg_eqv[no_vars]}+ −
@{thm [display] babs_simp[no_vars]}+ −
+ −
@{thm [display] ball_reg_right[no_vars]}+ −
@{thm [display] bex_reg_left[no_vars]}+ −
@{thm [display] bex1_bexeq_reg[no_vars]}+ −
+ −
*}+ −
+ −
subsection {* Injection *}+ −
+ −
text {*+ −
+ −
The 2 key lemmas are:+ −
+ −
@{thm [display] apply_rsp[no_vars]}+ −
@{thm [display] rep_abs_rsp[no_vars]}+ −
+ −
+ −
+ −
*}+ −
+ −
+ −
+ −
+ −
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+ −
(*>*)+ −