(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)
(*<*)
theory Paper
imports "Quotient"
"LaTeXsugar"
"../Nominal/FSet"
begin
notation (latex output)
rel_conj ("_ OOO _" [53, 53] 52) and
"op -->" (infix "\<rightarrow>" 100) and
"==>" (infix "\<Rightarrow>" 100) and
fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and
fun_rel ("_ \<^raw:\mbox{\doublearr}> _" 51) and
list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
fempty ("\<emptyset>") and
funion ("_ \<union> _") and
finsert ("{_} \<union> _") and
Cons ("_::_") and
concat ("flat") and
fconcat ("\<Union>")
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 {*
\begin{flushright}
{\em ``Not using a [quotient] package has its advantages: we do not have to\\
collect all the theorems we shall ever want into one giant list;''}\\
Larry Paulson \cite{Paulson06}
\end{flushright}
\noindent
Isabelle is a popular 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 how to use both mechanisms for dealing with quotient
constructions in HOL (see \cite{Homeier05,Paulson06}). For example the
integers in Isabelle/HOL are constructed by a quotient construction over the
type @{typ "nat \<times> nat"} and the equivalence relation
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}\hfill\numbered{natpairequiv}
\end{isabelle}
\noindent
This constructions yields the new type @{typ int} and definitions for @{text
"0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in
terms of operations on pairs of natural numbers (namely @{text
"add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).
Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"},
by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}
\end{isabelle}
\noindent
which states that two lists are equivalent if every element in one list is
also member in the other. The empty finite set, written @{term "{||}"}, can
then be defined as the empty list and the union of two finite sets, written
@{text "\<union>"}, as list append.
An area where quotients are ubiquitous is reasoning about programming language
calculi. A simple example is the lambda-calculus, whose raw terms are defined as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
\end{isabelle}
\noindent
The problem with this definition arises when one attempts to
prove formally, for example, the substitution lemma \cite{Barendregt81} by induction
over the structure of terms. This can be fiendishly complicated (see
\cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof
about raw lambda-terms). In contrast, if we reason about
$\alpha$-equated lambda-terms, that means terms quotient according to
$\alpha$-equivalence, then the reasoning infrastructure provided,
for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal
proof of the substitution lemma almost trivial.
The difficulty is that in order to be able to reason about integers, finite
sets or $\alpha$-equated lambda-terms one needs to establish a reasoning
infrastructure by transferring, or \emph{lifting}, definitions and theorems
from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}
(similarly for finite sets and $\alpha$-equated lambda-terms). This lifting
usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}.
It is feasible to to this work manually, if one has only a few quotient
constructions at hand. But if they have to be done over and over again, as in
Nominal Isabelle, then manual reasoning is not an option.
The purpose of a \emph{quotient package} is to ease the lifting of theorems
and automate the reasoning as much as possible. In the
context of HOL, there have been a few quotient packages already
\cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
\cite{Homeier05} implemented in HOL4. The fundamental construction these
quotient packages perform can be illustrated by the following picture:
\begin{center}
\mbox{}\hspace{20mm}\begin{tikzpicture}
%%\draw[step=2mm] (-4,-1) grid (4,1);
\draw[very thick] (0.7,0.3) circle (4.85mm);
\draw[rounded corners=1mm, very thick] ( 0.0,-0.9) rectangle ( 1.8, 0.9);
\draw[rounded corners=1mm, very thick] (-1.95,0.8) rectangle (-2.9,-0.195);
\draw (-2.0, 0.8) -- (0.7,0.8);
\draw (-2.0,-0.195) -- (0.7,-0.195);
\draw ( 0.7, 0.23) node {\begin{tabular}{@ {}c@ {}}equiv-\\[-1mm]clas.\end{tabular}};
\draw (-2.45, 0.35) node {\begin{tabular}{@ {}c@ {}}new\\[-1mm]type\end{tabular}};
\draw (1.8, 0.35) node[right=-0.1mm]
{\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw elements)\end{tabular}};
\draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
\draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36);
\draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);
\draw (-0.95, 0.26) node[above=0.4mm] {@{text Rep}};
\draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}};
\end{tikzpicture}
\end{center}
\noindent
The starting point is an existing type, to which we refer as the
\emph{raw type}, over which an equivalence relation given by the user is
defined. With this input the package introduces a new type, to which we
refer as the \emph{quotient type}. This type comes with an
\emph{abstraction} and a \emph{representation} function, written @{text Abs}
and @{text Rep}.\footnote{Actually slightly more basic functions are given;
the functions @{text Abs} and @{text Rep} need to be derived from them. We
will show the details later. } These functions relate elements in the
existing type to ones in the new type and vice versa; they can be uniquely
identified by their type. For example for the integer quotient construction
the types of @{text Abs} and @{text Rep} are
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
\end{isabelle}
\noindent
We therefore often write @{text Abs_int} and @{text Rep_int} if the
typing information is important.
Every abstraction and representation function stands for an isomorphism
between the non-empty subset and elements in the new type. They are
necessary for making definitions involving the new type. For example @{text
"0"} and @{text "1"} of type @{typ int} can be defined as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "0 \<equiv> Abs_int (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs_int (1, 0)"}
\end{isabelle}
\noindent
Slightly more complicated is the definition of @{text "add"} having type
@{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows
@{text [display, indent=10] "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
\noindent
where we take the representation of the arguments @{text n} and @{text m},
add them according to the function @{text "add_pair"} and then take the
abstraction of the result. This is all straightforward and the existing
quotient packages can deal with such definitions. But what is surprising
that none of them can deal with slightly more complicated definitions involving
\emph{compositions} of quotients. Such compositions are needed for example
in case of quotienting lists to yield finite sets and the operator that
flattens lists of lists, defined as follows
@{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
\noindent
We expect that the corresponding operator on finite sets, written @{term "fconcat"},
builds finite unions of finite sets:
@{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
\noindent
The quotient package should provide us with a definition for @{text "\<Union>"} in
terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is
that the method used in the existing quotient
packages of just taking the representation of the arguments and then taking
the abstraction of the result is \emph{not} enough. The reason is that case in case
of @{text "\<Union>"} we obtain the incorrect definition
@{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
\noindent
where the right-hand side is not even typable! This problem can be remedied in the
existing quotient packages by introducing an intermediate step and reasoning
about flattening of lists of finite sets. However, this remedy is rather
cumbersome and inelegant in light of our work, which can deal with such
definitions directly. The solution is that we need to build aggregate
representation and abstraction functions, which in case of @{text "\<Union>"}
generate the following definition
@{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map Rep_fset \<circ> Rep_fset) S))"}
\noindent
where @{term map} is the usual mapping function for lists. In this paper we
will present a formal definition of our aggregate abstraction and
representation functions (this definition was omitted in \cite{Homeier05}).
They generate definitions, like the one above for @{text "\<Union>"},
according to the type of the raw constant and the type
of the quotient constant. This means we also have to extend the notions
of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
from Homeier \cite{Homeier05}.
We are also able to address the criticism by Paulson \cite{Paulson06} cited
at the beginning of this section about having to collect theorems that are
lifted from the raw level to the quotient level into one giant list. Our
quotient package is the first one that is modular so that it allows to lift
single theorems separately. This has the advantage for the user to develop a
formal theory interactively an a natural progression. A pleasing result of
the modularity is also that we are able to clearly specify what needs to be
done in the lifting process (this was only hinted at in \cite{Homeier05} and
implemented as a ``rough recipe'' in ML-code).
The paper is organised as follows: Section \ref{sec:prelims} presents briefly
some necessary preliminaries; Section \ref{sec:type} describes the definitions
of quotient types and shows how definition of constants can be made over
quotient types. \ldots
*}
section {* Preliminaries and General Quotient\label{sec:prelims} *}
text {*
In this section we present the definitions of a quotient that follow
closely those given by Homeier.
\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}
Higher Order Logic
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}
{\it Say more about containers / maping functions }
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.
{\it say something about our use of @{text "\<sigma>s"}}
*}
section {* Quotient Types and Quotient Definitions\label{sec:type} *}
text {*
The first step in a quotient construction is to take a name for the new
type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence
relation must be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
the declaration is therefore
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}
\end{isabelle}
\noindent
and a proof that @{text "R"} is indeed an equivalence relation. Two concrete
examples are
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
\isacommand{quotient\_type}~~@{text "int = nat \<times> nat / \<approx>\<^bsub>nat \<times> nat\<^esub>"}\\
\isacommand{quotient\_type}~~@{text "\<alpha> fset = \<alpha> list / \<approx>\<^bsub>list\<^esub>"}
\end{tabular}
\end{isabelle}
\noindent
which introduce the type of integers and of finite sets using the
equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text
"\<approx>\<^bsub>list\<^esub>"} defined earlier in \eqref{natpairequiv} and
\eqref{listequiv}, respectively (the proofs about being equivalence
relations is omitted). Given this data, we declare internally
the quotient types as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
\end{isabelle}
\noindent
where the right-hand side is the (non-empty) set of equivalence classes of
@{text "R"}. The restriction in this declaration is that the type variables
in the raw type @{text "\<sigma>"} must be included in the type variables @{text
"\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will provide us with the following
abstraction and representation functions having the type
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "abs_\<kappa>\<^isub>q :: \<sigma> set \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}\hspace{10mm}@{text "rep_\<kappa>\<^isub>q :: \<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma> set"}
\end{isabelle}
\noindent
They relate the new quotient type and equivalence classes of the raw
type. However, as Homeier \cite{Homeier05} noted, it is much more convenient
to work with the following derived abstraction and representation functions
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "Abs_\<kappa>\<^isub>q x \<equiv> abs_\<kappa>\<^isub>q (R x)"}\hspace{10mm}@{text "Rep_\<kappa>\<^isub>q x \<equiv> \<epsilon> (rep_\<kappa>\<^isub>q x)"}
\end{isabelle}
\noindent
on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"} in the
definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the
quotient type and the raw type directly, as can be seen from their type,
namely @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},
respectively. Given that @{text "R"} is an equivalence relation, the
following property
@{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
\noindent
holds (for the proof see \cite{Homeier05}) for every quotient type defined
as above.
The next step in a quotient construction is to introduce definitions of new constants
involving the quotient type. These definitions need to be given in terms of concepts
of the raw type (remember this is the only way how to extend HOL
with new definitions). For the user visible is the declaration
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
\end{isabelle}
\noindent
where @{text t} is the definiens (its type @{text \<sigma>} can always be inferred)
and @{text "c"} is the name of definiendum, whose type @{text "\<tau>"} needs to be
given explicitly (the point is that @{text "\<tau>"} and @{text "\<sigma>"} can only differ
in places where a quotient and raw type are involved). Two concrete examples are
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
\isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\
\isacommand{quotient\_definition}~~@{text "\<Union> :: (\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}~~%
\isacommand{is}~~@{text "flat"}
\end{tabular}
\end{isabelle}
\noindent
The first one declares zero for integers and the second the operator for
building unions of finite sets.
The problem for us is that from such declarations we need to derive proper
definitions using the @{text "Abs"} and @{text "Rep"} functions for the
quotient types involved. The data we rely on is the given quotient type
@{text "\<tau>"} and the raw type @{text "\<sigma>"}. They allow us to define \emph{aggregate
abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
\<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we given below. The idea behind
these two functions is to recursively descend into the raw types @{text \<sigma>} and
quotient types @{text \<tau>}, and generate the appropriate
@{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
we generate just the identity whenever the types are equal. All clauses
are as follows:
\begin{center}
\begin{tabular}{rcl}
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
@{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
@{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\
@{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
@{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\
@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
\end{tabular}\hfill\numbered{ABSREP}
\end{center}
%
\noindent
where in the last two clauses we have that the quotient type @{text "\<alpha>s
\<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
@{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
list"}). The quotient construction ensures that the type variables in @{text
"\<rho>s"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
matchers for the @{text "\<alpha>s"} when matching @{text "\<rho>s \<kappa>"} against
@{text "\<sigma>s \<kappa>"}. The
function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
type as follows:
%
\begin{center}
\begin{tabular}{rcl}
@{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
@{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\
@{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
@{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}
\end{tabular}
\end{center}
%
\noindent
In this definition we abuse the fact that we can interpret type-variables @{text \<alpha>} as
term variables @{text a}. In the last clause we build an abstraction over all
term-variables inside map-function generated by the auxiliary function
@{text "MAP'"}.
The need of aggregate map-functions can be seen in cases where we build quotients,
say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}.
In this case @{text MAP} generates the
aggregate map-function:
@{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}
\noindent
which we need to define the aggregate abstraction and representation functions.
To see how these definitions pan out in practise, let us return to our
example about @{term "concat"} and @{term "fconcat"}, where we have the raw type
@{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
fset"}. Feeding them into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
the abstraction function
@{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}
\noindent
In our implementation we further
simplify this function by rewriting with the usual laws about @{text
"map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f \<circ> id =
id \<circ> f = f"}. This gives us the abstraction function
@{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
\noindent
which we can use for defining @{term "fconcat"} as follows
@{text [display, indent=10] "\<Union> \<equiv> ((map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
\noindent
Note that by using the operator @{text "\<singlearr>"} and special clauses
for function types in \eqref{ABSREP}, we do not have to
distinguish between arguments and results: the representation and abstraction
functions are just inverses of each other, which we can combine using
@{text "\<singlearr>"} to deal uniformly with arguments of functions and
their result. Consequently, all definitions in the quotient package
are of the general form
@{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
\noindent
where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
type of the defined quotient constant @{text "c"}. This data can be easily
generated from the declaration given by the user.
To increase the confidence of making correct definitions, we can prove
that the terms involved are all typable.
\begin{lemma}
If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"}
and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"},
then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type
@{text "\<tau> \<Rightarrow> \<sigma>"}.
\end{lemma}
\begin{proof}
By induction and analysing the definitions of @{text "ABS"}, @{text "REP"}
and @{text "MAP"}. The cases of equal types and function types are
straightforward (the latter follows from @{text "\<singlearr>"} having the
type @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). In case of equal type
constructors we can observe that a map-function after applying the functions
@{text "ABS (\<sigma>s, \<tau>s)"} produces a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}. The
interesting case is the one with unequal type constructors. Since we know
the quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have
that @{text "Abs_\<kappa>\<^isub>q"} is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s
\<kappa>\<^isub>q"}. This type can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s
\<kappa>\<^isub>q"} where the type variables @{text "\<alpha>s"} are instantiated with the
@{text "\<tau>s"}. The complete type can be calculated by observing that @{text
"MAP (\<rho>s \<kappa>)"}, after applying the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it,
returns a term of type @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is
equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with
@{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed
\end{proof}
\noindent
The reader should note that this lemma fails for the abstraction and representation
functions used, for example, in Homeier's quotient package.
*}
section {* Respectfulness and Preservation *}
text {*
The main point of the quotient package is to automatically ``lift'' theorems
involving constants over the raw type to theorems involving constants over
the quotient type. Before we can describe this lift process, we need to impose
some restrictions. The reason is that even if definitions for all raw constants
can be given, \emph{not} all theorems can be actually be lifted. Most notably is
the bound variable function, that is the constant @{text bn}, defined for
raw lambda-terms as follows
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "bn (x) \<equiv> \<emptyset>"}\hspace{5mm}
@{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{5mm}
@{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
\end{isabelle}
\noindent
This constant just does not respect @{text "\<alpha>"}-equivalence and as
consequently no theorem involving this constant can be lifted to @{text
"\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of
the properties of \emph{respectfullness} and \emph{preservation}. We have
to slighlty extend Homeier's definitions in order to deal with quotient
compositions.
To formally define what respectfulness is, we have to first define
the notion of \emph{aggregate equivalence relations}.
@{text [display] "GIVE DEFINITION HERE"}
class returned by this constant depends only on the equivalence
classes of the arguments applied to the constant. To automatically
lift a theorem that talks about a raw constant, to a theorem about
the quotient type a respectfulness theorem is required.
A respectfulness condition for a constant can be expressed in
terms of an aggregate relation between the constant and itself,
for example the respectfullness for @{text "append"}
can be stated as:
@{text [display, indent=10] "(R \<doublearr> R \<doublearr> R) append append"}
\noindent
Which after unfolding the definition of @{term "op ===>"} is equivalent to:
@{thm [display, indent=10] append_rsp_unfolded[no_vars]}
\noindent An aggregate relation is defined in terms of relation
composition, so we define it first:
\begin{definition}[Composition of Relations]
@{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate
composition @{thm pred_compI[no_vars]}
\end{definition}
The aggregate relation for an aggregate raw type and quotient type
is defined as:
\begin{itemize}
\item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}
\item @{text "REL(\<sigma>, \<sigma>)"} = @{text "op ="}
\item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
\item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<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}
Again, the last case is novel, so lets look at the example of
respectfullness for @{term concat}. The statement according to
the definition above is:
@{thm [display, indent=10] 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, indent=10] 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}.
*}
text {*
Sometimes a non-lifted polymorphic constant is instantiated to a
type being lifted. For example take the @{term "op #"} which inserts
an element in a list of pairs of natural numbers. When the theorem
is lifted, the pairs of natural numbers are to become integers, but
the head constant is still supposed to be the head constant, just
with a different type. To be able to lift such theorems
automatically, additional theorems provided by the user are
necessary, we call these \emph{preservation} theorems following
Homeier's naming.
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, indent=10] (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, indent=10] 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 as defined above
and the abstraction and relation functions are the ones of the sub
quotients composed with the usual function composition.
The @{term "Rep"} and @{term "Abs"} functions that we obtain agree
with the definition of aggregate Abs/Rep 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 flat}. To be able to lift
theorems that talk about it we provide 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 of 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 were 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, as all three
can be performed independently from each other.
*}
subsection {* Regularization and Injection statements *}
text {*
We first define the function @{text REG}, which takes the statements
of the raw theorem and the lifted theorem (both as terms) and
returns the statement of the regularized version. The intuition
behind this function 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{center}
\begin{tabular}{rcl}
\multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\
@{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\
@{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
@{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\
@{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\
@{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\
@{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\
@{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
@{text "REG (v\<^isub>1, v\<^isub>2)"} & $\dn$ & @{text "v\<^isub>1"}\\
@{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\
\end{tabular}
\end{center}
In the above definition we omitted the cases for existential quantifiers
and unique existential quantifiers, as they are very similar to the cases
for the universal quantifier.
Next we define the function @{text INJ} which takes the statement of
the regularized theorems and the statement of the lifted theorem both as
terms and returns the statement of the injected theorem:
\begin{center}
\begin{tabular}{rcl}
\multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\
@{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) "} & $\dn$ & @{text "\<lambda>x. INJ (t, s)"}\\
@{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}\\
@{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
@{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> (INJ (t, s))"}\\
@{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\
@{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} & $\dn$ & @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
@{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) "} & $\dn$ & @{text "v\<^isub>1"}\\
@{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}\\
@{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) "} & $\dn$ & @{text "c\<^isub>1"}\\
@{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}\\
\end{tabular}
\end{center}
For existential quantifiers and unique existential quantifiers it is
defined similarly to the universal one.
*}
subsection {* Proof procedure *}
(* In the below the type-guiding 'QuotTrue' assumption is removed. We need it
only for bound variables without types, while in the paper presentation
variables are typed *)
text {*
With the above definitions of @{text "REG"} and @{text "INJ"} we can show
how the proof is performed. The first step is always the application of
of the following lemma:
@{term [display, indent=10] "[|A; A --> B; B = C; C = D|] ==> D"}
With @{text A} instantiated to the original raw theorem,
@{text B} instantiated to @{text "REG(A)"},
@{text C} instantiated to @{text "INJ(REG(A))"},
and @{text D} instantiated to the statement of the lifted theorem.
The first assumption can be immediately discharged using the original
theorem and the three left subgoals are exactly the subgoals of regularization,
injection and cleaning. The three can be proved independently by the
framework and in case there are non-solved subgoals they can be left
to the user.
The injection and cleaning subgoals are always solved if the appropriate
respectfulness and preservation theorems are given. It is not the case
with regularization; sometimes a theorem given by the user does not
imply a regularized version and a stronger one needs to be proved. This
is outside of the scope of the quotient package, so such obligations are
left to the user. Take a simple statement for integers @{term "0 \<noteq> 1"}.
It does not follow from the fact that @{term "\<not> (0, 0) = (1, 0)"} because
of regularization. The raw theorem only shows that particular items in the
equivalence classes are not equal. A more general statement saying that
the classes are not equal is necessary.
*}
subsection {* Proving Regularization *}
text {*
Isabelle provides a set of \emph{mono} rules, that are used to split implications
of similar statements into simpler implication subgoals. These are enhanced
with special quotient theorem in the regularization goal. Below we only show
the versions for the universal quantifier. For the existential quantifier
and abstraction they are analogous.
First, bounded universal quantifiers can be removed on the right:
@{thm [display, indent=10] ball_reg_right[no_vars]}
They can be removed anywhere if the relation is an equivalence relation:
@{thm [display, indent=10] ball_reg_eqv[no_vars]}
And finally it can be removed anywhere if @{term R2} is an equivalence relation, then:
@{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]}
The last theorem is new in comparison with Homeier's package. There the
injection procedure would be used to prove goals with such shape, and there
the equivalence assumption would be used. We use the above theorem directly
also for composed relations where the range type is a type for which we know an
equivalence theorem. This allows separating regularization from injection.
*}
(*
@{thm bex_reg_eqv_range[no_vars]}
@{thm [display] bex_reg_left[no_vars]}
@{thm [display] bex1_bexeq_reg[no_vars]}
@{thm [display] bex_reg_eqv[no_vars]}
@{thm [display] babs_reg_eqv[no_vars]}
@{thm [display] babs_simp[no_vars]}
*)
subsection {* Injection *}
text {*
The injection proof starts with an equality between the regularized theorem
and the injected version. The proof again follows by the structure of the
two terms, and is defined for a goal being a relation between these two terms.
\begin{itemize}
\item For two constants, an appropriate constant respectfullness assumption is used.
\item For two variables, we use the assumptions proved in regularization.
\item For two abstractions, they are eta-expanded and beta-reduced.
\end{itemize}
Otherwise the two terms are applications. There are two cases: If there is a REP/ABS
in the injected theorem we can use the theorem:
@{thm [display, indent=10] rep_abs_rsp[no_vars]}
\noindent
and continue the proof.
Otherwise we introduce an appropriate relation between the subterms and continue with
two subgoals using the lemma:
@{thm [display, indent=10] apply_rsp[no_vars]}
*}
subsection {* Cleaning *}
text {*
The @{text REG} and @{text INJ} functions have been defined in such a way
that establishing the goal theorem now consists only on rewriting the
injected theorem with the preservation theorems.
\begin{itemize}
\item First for lifted constants, their definitions are the preservation rules for
them.
\item For lambda abstractions lambda preservation establishes
the equality between the injected theorem and the goal. This allows both
abstraction and quantification over lifted types.
@{thm [display] (concl) lambda_prs[no_vars]}
\item Relations over lifted types are folded with:
@{thm [display] (concl) Quotient_rel_rep[no_vars]}
\item User given preservation theorems, that allow using higher level operations
and containers of types being lifted. An example may be
@{thm [display] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}
\end{itemize}
*}
section {* Examples *}
(* Mention why equivalence *)
text {*
In this section we will show, a complete interaction with the quotient package
for defining the type of integers by quotienting pairs of natural numbers and
lifting theorems to integers. Our quotient package is fully compatible with
Isabelle type classes, but for clarity we will not use them in this example.
In a larger formalization of integers using the type class mechanism would
provide many algebraic properties ``for free''.
A user of our quotient package first needs to define a relation on
the raw type, by which the quotienting will be performed. We give
the same integer relation as the one presented in the introduction:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\isacommand{fun}~~@{text "int_rel"}~~\isacommand{where}~~@{text "(m \<Colon> nat, n) int_rel (p, q) = (m + q = n + p)"}
\end{isabelle}
\noindent
Next the quotient type is defined. This leaves a proof obligation that the
relation is an equivalence relation which is solved automatically using the
definitions:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}
\end{isabelle}
\noindent
The user can then specify the constants on the quotient type:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\begin{tabular}{@ {}l}
\isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\
\isacommand{fun}~~@{text "plus_raw"}~~\isacommand{where}~~@{text "plus_raw (m :: nat, n) (p, q) = (m + p, n + q)"}\\
\isacommand{quotient\_definition}~~@{text "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)"}~~\isacommand{is}~~@{text "plus_raw"}\\
\end{tabular}
\end{isabelle}
\noindent
Lets first take a simple theorem about addition on the raw level:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\isacommand{lemma}~~@{text "plus_zero_raw: int_rel (plus_raw (0, 0) x) x"}
\end{isabelle}
\noindent
When the user tries to lift a theorem about integer addition, the respectfulness
proof obligation is left, so let us prove it first:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\isacommand{lemma}~~@{text "[quot_respect]: (int_rel \<Longrightarrow> int_rel \<Longrightarrow> int_rel) plus_raw plus_raw"}
\end{isabelle}
\noindent
Can be proved automatically by the system just by unfolding the definition
of @{text "op \<Longrightarrow>"}.
Now the user can either prove a lifted lemma explicitly:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting plus_zero_raw"}
\end{isabelle}
\noindent
Or in this simple case use the automated translation mechanism:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\isacommand{thm}~~@{text "plus_zero_raw[quot_lifted]"}
\end{isabelle}
\noindent
obtaining the same result.
*}
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}
*}
section {* Conclusion *}
text {*
The code of the quotient package described here is already included in the
standard distribution of Isabelle.\footnote{Avaiable from
\href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is
heavily used in Nominal Isabelle, which provides a convenient reasoning
infrastructure for programming language calculi involving binders. Earlier
versions of Nominal Isabelle have been used successfully in formalisations
of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08},
Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for
concurrency \cite{BengtsonParow09} and a strong normalisation result for
cut-elimination in classical logic \cite{UrbanZhu08}.
*}
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, Quotients and maps
can be defined 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}
*}
(*<*)
end
(*>*)