(*<*)
theory Paper
imports "Quotient"
"LaTeXsugar"
"../Nominal/FSet"
begin
(****
** things to do for the next version
*
* - what are quot_thms?
* - what do all preservation theorems look like
*)
notation (latex output)
rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
"op -->" (infix "\<longrightarrow>" 100) and
"==>" (infix "\<Longrightarrow>" 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.
Quotients are important in a variety of areas, but they are really ubiquitous in
the area of 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, for instance, when one attempts to
prove formally 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 do 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} and 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. } They relate elements in the
existing type to elements in the new type and vice versa, and can be uniquely
identified by their quotient 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
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
\hfill\numbered{adddef}
\end{isabelle}
\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 automatically 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 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}.
In addition we are 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 higher-order theorems separately. This has the advantage for the user of being able to develop a
formal theory interactively as a natural progression. A pleasing side-result of
the modularity is that we are able to clearly specify what is involved
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 definitions of constants can be made over
quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
and preservation; Section \ref{sec:lift} describes the lifting of theorems;
Section \ref{sec:examples} presents some examples
and Section \ref{sec:conc} concludes and compares our results to existing
work.
*}
section {* Preliminaries and General Quotients\label{sec:prelims} *}
text {*
We give in this section a crude overview of HOL and describe the main
definitions given by Homeier for quotients \cite{Homeier05}.
At its core, HOL is based on a simply-typed term language, where types are
recorded in Church-style fashion (that means, we can always infer the type of
a term and its subterms without any additional information). The grammars
for types and terms are as follows
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}rl@ {\hspace{3mm}}l@ {}}
@{text "\<sigma>, \<tau> ::="} & @{text "\<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} & (type variables and type constructors)\\
@{text "t, s ::="} & @{text "x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"} &
(variables, constants, applications and abstractions)\\
\end{tabular}
\end{isabelle}
\noindent
We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and
@{text "\<sigma>s"} to stand for collections of type variables and types,
respectively. The type of a term is often made explicit by writing @{text
"t :: \<sigma>"}. HOL includes a type @{typ bool} for booleans and the function
type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains many primitive and defined
constants; a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
bool"}, and the identity function with type @{text "id :: \<sigma> => \<sigma>"} is
defined as @{text "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).
An important point to note is that theorems in HOL can be seen as a subset
of terms that are constructed specially (namely through axioms and prove
rules). As a result we are able to define automatic proof
procedures showing that one theorem implies another by decomposing the term
underlying the first theorem.
Like Homeier, our work relies on map-functions defined for every type
constructor taking some arguments, for example @{text map} for lists. Homeier
describes in \cite{Homeier05} map-functions for products, sums, options and
also the following map for function types
@{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}
\noindent
Using this map-function, we can give the following, equivalent, but more
uniform, definition for @{text add} shown in \eqref{adddef}:
@{text [display, indent=10] "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
\noindent
Using extensionality and unfolding the definition of @{text "\<singlearr>"},
we can get back to \eqref{adddef}.
In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function
of the type-constructor @{text \<kappa>}. In our implementation we maintain
a database of these map-functions that can be dynamically extended.
It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"},
which define equivalence relations in terms of constituent equivalence
relations. For example given two equivalence relations @{text "R\<^isub>1"}
and @{text "R\<^isub>2"}, we can define an equivalence relations over
products as follows
%
@{text [display, indent=10] "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}
\noindent
Homeier gives also the following operator for defining equivalence
relations over function types
%
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}
\hfill\numbered{relfun}
\end{isabelle}
\noindent
In the context of quotients, the following two notions from are \cite{Homeier05}
needed later on.
\begin{definition}[Respects]\label{def:respects}
An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.
\end{definition}
\begin{definition}[Bounded Quantification and Bounded Abstractions]\label{def:babs}
@{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}.
\end{definition}
The central definition in Homeier's work \cite{Homeier05} relates equivalence
relations, abstraction and representation functions:
\begin{definition}[Quotient Types]
Given a relation $R$, an abstraction function $Abs$
and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"}
means
\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}
\noindent
The value of this definition is that validity of @{text "Quotient R Abs Rep"} can
often be proved in terms of the validity of @{text "Quotient"} over the constituent
types of @{text "R"}, @{text Abs} and @{text Rep}.
For example Homeier proves the following property for higher-order quotient
types:
\begin{proposition}\label{funquot}
@{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"
and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
\end{proposition}
\noindent
As a result, Homeier is able to build an automatic prover that can nearly
always discharge a proof obligation involving @{text "Quotient"}. Our quotient
package makes heavy
use of this part of Homeier's work including an extension
to deal with compositions of equivalence relations defined as follows:
\begin{definition}[Composition of Relations]
@{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
composition defined by @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
holds if and only if @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and
@{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}.
\end{definition}
\noindent
Unfortunately, there are two predicaments with compositions of relations.
First, a general quotient theorem, like the one given in Proposition \ref{funquot},
cannot be stated inside HOL, because of the restriction on types.
Second, even if we were able to state such a quotient theorem, it
would not be true in general. However, we can prove specific instances of a
quotient theorem for composing particular quotient relations.
To lift @{term flat} the quotient theorem for composing @{text "\<approx>\<^bsub>list\<^esub>"}
is necessary:
% It says when lists are being quotiented to finite sets,
% the contents of the lists can be quotiented as well
If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"} then
@{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
\vspace{-.5mm}
*}
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 @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
the quotient type declaration is therefore
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}\hfill\numbered{typedecl}
\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 in \eqref{natpairequiv} and
\eqref{listequiv}, respectively (the proofs about being equivalence
relations is omitted). Given this data, we define for declarations shown in
\eqref{typedecl} the quotient types internally 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 constraint 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 then provide us with the following
abstraction and representation functions
\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
As can be seen from the type, 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 holds for every quotient type
(for the proof see \cite{Homeier05}).
\begin{proposition}
@{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
\end{proposition}
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 the visible part of such definitions 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 is 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 (@{text "flat"} having the type
@{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}).
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 give below. The idea behind
these two functions is to simultaneously 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. On the ``way'' down,
however we might have to use map-functions to let @{text Abs} and @{text Rep} act
over the appropriate types. In what follows we use the short-hand notation
@{text "ABS (\<sigma>s, \<tau>s)"} to mean @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>i, \<tau>\<^isub>i)"}; similarly
for @{text REP}.
%
\begin{center}
\hfill
\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
In the last two clauses we have that the 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 rely on 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 of the map-function generated by the auxiliary function
@{text "MAP'"}.
The need for 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 is essential in order to define the corresponding 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 these types 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 simpler 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, but can deal with them uniformly.
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 in this way of making 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 mutual induction and analysing the definitions of @{text "ABS"} and @{text "REP"}.
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 in Homeier's quotient package.
*}
section {* Respectfulness and Preservation \label{sec:resp} *}
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 lifting process, we need to impose
two restrictions in the form of proof obligations that arise during the
lifting. The reason is that even if definitions for all raw constants
can be given, \emph{not} all theorems can be lifted to the quotient type. 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{4mm}
@{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}
@{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
\end{isabelle}
\noindent
We can generate a definition for this constant using @{text ABS} and @{text REP}.
But this constant does \emph{not} respect @{text "\<alpha>"}-equivalence and
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{respectfulness} and \emph{preservation}. We have
to slightly 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} using @{text REL}:
\begin{center}
\hfill
\begin{tabular}{rcl}
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
@{text "REL (\<sigma>, \<sigma>)"} & $\dn$ & @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\smallskip\\
@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
\end{tabular}\hfill\numbered{REL}
\end{center}
\noindent
The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:
we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type
@{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are determined by matching
@{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
Lets return to the lifting procedure of theorems. Assume we have a theorem
that contains the raw constant @{text "c\<^isub>r :: \<sigma>"} and which we want to
lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation
we throw the following proof obligation
@{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
%%% PROBLEM I do not yet completely understand the
%%% form of respectfulness theorems
%%%\noindent
%%%if @ {text \<sigma>} and @ {text \<tau>} have no type variables. In case they have, then
%%%the proof obligation is of the form
%%%
%%%@ {text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
%%% ANSWER: The respectfulness theorems never have any quotient assumptions,
%%% So the commited version is ok.
\noindent
%%%where @ {text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.
Homeier calls these proof obligations \emph{respectfulness
theorems}. However, unlike his quotient package, we might have several
respectfulness theorems for one constant---he has at most one.
The reason is that because of our quotient compositions, the types
@{text \<sigma>} and @{text \<tau>} are not completely determined by the type of @{text "c\<^bsub>r\<^esub>"}.
And for every instantiation of the types, we might end up with a
corresponding respectfulness theorem.
Before lifting a theorem, we require the user to discharge
them. And the point with @{text bn} is that the respectfulness theorem
looks as follows
@{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
\noindent
and the user cannot discharge it---because it is not true. To see this,
we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun}
using extensionally to obtain
@{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 implies bn(t\<^isub>1) = bn(t\<^isub>2)"}
\noindent
In contrast, if we lift a theorem about @{text "append"} to a theorem describing
the union of finite sets, then we need to discharge the proof obligation
@{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
\noindent
To do so, we have to establish
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
if @{thm (prem1) append_rsp_unfolded[of xs ys us vs, no_vars]} and
@{thm (prem2) append_rsp_unfolded[of xs ys us vs, no_vars]}
then @{thm (concl) append_rsp_unfolded[of xs ys us vs, no_vars]}
\end{isabelle}
\noindent
which is straightforward given the definition shown in \eqref{listequiv}.
The second restriction we have to impose arises from
non-lifted polymorphic constants, which are instantiated to a
type being quotient. For example, take the @{term "cons"} to
add a pair of natural numbers to a list. The pair of natural numbers
is to become an integer. But we still want to use @{text cons} for
adding integers to lists---just with a different type.
To be able to lift such theorems, we need a \emph{preservation theorem}
for @{text cons}. Assuming we have a polymorphic raw constant
@{text "c\<^isub>r :: \<sigma>"} and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"},
then a preservation theorem is as follows
@{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
\noindent
where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have
@{text [display, indent=10] "(Rep ---> map Rep ---> map Abs) cons = cons"}
\noindent
under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have
an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated
with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
then we need to show the corresponding preservation lemma.
%%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
%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
%theorem which allows quotienting inside the container:
%
%If @ {term R} is an equivalence relation and @ {term "Quotient R Abs Rep"}
%then
%
%@ {text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
%%%
%%%\noindent
%%%this theorem will then instantiate the quotients needed in the
%%%injection and cleaning proofs allowing the lifting procedure to
%%%proceed in an unchanged way.
*}
section {* Lifting of Theorems\label{sec:lift} *}
text {*
The main benefit of a quotient package is to lift automatically theorems over raw
types to theorems over quotient types. We will perform this lifting in
three phases, called \emph{regularization},
\emph{injection} and \emph{cleaning}.
The purpose of regularization is to change the quantifiers and abstractions
in a ``raw'' theorem to quantifiers over variables that respect the relation
(Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}
and @{term Abs} of appropriate types in front of constants and variables
of the raw type so that they can be replaced by the ones that include the
quotient type. The purpose of cleaning is to bring the theorem derived in the
first two phases into the form the user has specified. Abstractly, our
package establishes the following three proof steps:
\begin{center}
\begin{tabular}{r@ {\hspace{4mm}}l}
1.) & @{text "raw_thm \<longrightarrow> reg_thm"}\\
2.) & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\
3.) & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\
\end{tabular}
\end{center}
\noindent
In contrast to other quotient packages, our package requires
the \emph{term} of the @{text "quot_thm"} to be given by the user.\footnote{Though we
also provide a fully automated mode, where the @{text "quot_thm"} is guessed
from @{text "raw_thm"}.} As a result, it is possible that a user can lift only some
occurrences of a raw type.
The second and third proof step will always succeed if the appropriate
respectfulness and preservation theorems are given. In contrast, the first
proof step can fail: a theorem given by the user does not always
imply a regularized version and a stronger one needs to be proved. This
is outside of the scope where the quotient package can help. An example
for the failure is the simple statement for integers @{text "0 \<noteq> 1"}.
It does not follow by lifting from the fact that @{text "(0, 0) \<noteq> (1, 0)"}.
The raw theorem only shows that particular element in the
equivalence classes are not equal. A more general statement saying that
the equivalence classes are not equal is necessary.
In the following we will first define the statement of the
regularized theorem based on @{text "raw_thm"} and
@{text "quot_thm"}. Then we define the statement of the injected theorem, based
on @{text "reg_thm"} theorem and @{text "quot_thm"}. We then show the 3 proofs,
which can all be performed independently from each other.
We define the function @{text REG}. 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
equivalence relations. It is defined as follows:
\begin{center}
\begin{longtable}{rcl}
\multicolumn{3}{@ {}l}{abstractions:}\smallskip\\
@{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} & $\dn$ &
$\begin{cases}
@{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
\end{cases}$\smallskip\\
\\
\multicolumn{3}{@ {}l}{universal quantifiers:}\\
@{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} & $\dn$ &
$\begin{cases}
@{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "\<forall>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
\end{cases}$\smallskip\\
\multicolumn{3}{@ {}l}{equality:}\smallskip\\
%% REL of two equal types is the equality so we do not need a separate case
@{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\
\multicolumn{3}{@ {}l}{applications, variables and 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 (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\
@{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\[-5mm]
\end{longtable}
\end{center}
%
\noindent
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 as argument
@{text "reg_thm"} and @{text "quot_thm"} (both as
terms) and returns @{text "inj_thm"}:
\begin{center}
\begin{tabular}{rcl}
\multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions:}\\
@{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ &
$\begin{cases}
@{text "\<lambda>x. INJ (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x. INJ (t, s)))"}
\end{cases}$\\
@{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)))"}\smallskip\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{universal quantifiers:}\\
@{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"}\smallskip\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables and constants:}\smallskip\\
@{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 (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} & $\dn$ &
$\begin{cases}
@{text "x\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) x\<^isub>1)"}\\
\end{cases}$\\
@{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} & $\dn$ &
$\begin{cases}
@{text "c\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) c\<^isub>1)"}\\
\end{cases}$\\
\end{tabular}
\end{center}
\noindent
where again the cases for existential quantifiers and unique existential
quantifiers have been omitted.
In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always
start with an implication. Isabelle provides \emph{mono} rules that can split up
the implications into simpler implication subgoals. This succeeds for every
monotone connective, except in places where the function @{text REG} inserted,
for example, a quantifier by a bounded quantifier. In this case we have
rules of the form
@{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
\noindent
They decompose a bounded quantifier on the right-hand side. We can decompose a
bounded quantifier anywhere if R is an equivalence relation or
if it is a relation over function types with the range being an equivalence
relation. If @{text R} is an equivalence relation we can prove that
@{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}
\noindent
And when @{term R\<^isub>2} is an equivalence relation and we can prove
@{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
\noindent
The last theorem is new in comparison with Homeier's package. There the
injection procedure would be used to prove such goals, and there
the assumption about the equivalence relation would be used. We use the above theorem directly,
because this allows us to completely separate the first and the second
proof step into independent ``units''.
The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"}, starts with an equality.
The proof again follows the structure of the
two underlying terms, and is defined for a goal being a relation between these two terms.
\begin{itemize}
\item For two constants an appropriate constant respectfulness lemma is applied.
\item For two variables, we use the assumptions proved in the regularization step.
\item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.
\item For two applications, we check that the right-hand side is an application of
@{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"}. If yes then we
can apply the theorem:
@{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}
Otherwise we introduce an appropriate relation between the subterms
and continue with two subgoals using the lemma:
@{text [display, indent=10] "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
\end{itemize}
We defined the theorem @{text "inj_thm"} in such a way that
establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
definitions. Then all lifted constants, their definitions
are used to fold the @{term Rep} with the raw constant. Next for
all abstractions and quantifiers the lambda and
quantifier preservation theorems are used to replace the
variables that include raw types with respects by quantifiers
over variables that include quotient types. We show here only
the lambda preservation theorem. Given
@{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
@{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
\noindent
Next, relations over lifted types are folded to equalities.
For this the following theorem has been shown in Homeier~\cite{Homeier05}:
@{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
\noindent
Finally, we rewrite with the preservation theorems. This will result
in two equal terms that can be solved by reflexivity.
*}
section {* Examples \label{sec: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 \eqref{natpairequiv}:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\begin{tabular}{@ {}l}
\isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\
\isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}
\end{tabular}
\end{isabelle}
\noindent
Next the quotient type is defined. This generates a proof obligation that the
relation is an equivalence relation, which is solved automatically using the
definition and extensionality:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\begin{tabular}{@ {}l}
\isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}\\
\hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"}
\end{tabular}
\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)"}\\[3mm]
\isacommand{fun}~~@{text "plus_raw"}~~\isacommand{where}~~%
@{text "plus_raw (m, n) (p, q) = (m + p :: nat, n + q :: nat)"}\\
\isacommand{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~%
\isacommand{is}~~@{text "plus_raw"}\\
\end{tabular}
\end{isabelle}
\noindent
The following theorem about addition on the raw level can be proved.
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\isacommand{lemma}~~@{text "plus_zero_raw: int_rel (plus_raw (0, 0) x) x"}
\end{isabelle}
\noindent
If the user attempts to lift this theorem, all proof obligations are
automatically discharged, except the respectfulness
proof for @{text "plus_raw"}:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\begin{tabular}{@ {}l}
\isacommand{lemma}~~@{text "[quot_respect]:\\
(int_rel \<doublearr> int_rel \<doublearr> int_rel) plus_raw plus_raw"}
\end{tabular}
\end{isabelle}
\noindent
This can be discharged automatically by Isabelle when telling it to unfold the definition
of @{text "\<doublearr>"}.
After this, the user can prove the lifted lemma explicitly:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting plus_zero_raw"}
\end{isabelle}
\noindent
or by the completely automated mode by stating:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\isacommand{thm}~~@{text "plus_zero_raw[quot_lifted]"}
\end{isabelle}
\noindent
Both methods give the same result, namely
@{text [display, indent=10] "0 + x = x"}
\noindent
Although seemingly simple, arriving at this result without the help of a quotient
package requires substantial reasoning effort.
*}
section {* Conclusion and Related Work\label{sec:conc}*}
text {*
The code of the quotient package and the examples described here are
already included in the
standard distribution of Isabelle.\footnote{Available from
\href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is
heavily used in the new version of Nominal Isabelle, which provides a convenient reasoning
infrastructure for programming language calculi involving binders.
To achieve this, it builds types representing @{text \<alpha>}-equivalent terms.
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}.
There is a wide range of existing of literature for dealing with
quotients in theorem provers.
Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
defines quotient types for Isabelle/HOL. But he did not include theorem lifting.
Harrison's quotient package~\cite{harrison-thesis} is the first one that is
able to automatically lift theorems, however only first-order theorems (that is theorems
where abstractions, quantifiers and variables do not involve functions that
include the quotient type).
There is also some work on quotient types in
non-HOL based systems and logical frameworks, including theory interpretations
in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02},
and setoids in Coq \cite{ChicliPS02}.
Paulson showed a construction of quotients that does not require the
Hilbert Choice operator, but also only first-order theorems can be lifted~\cite{Paulson06}.
The most related work to our package is the package for HOL4 by Homeier~\cite{Homeier05}.
He introduced most of the abstract notions about quotients and also deals with the
lifting of higher-order theorems. However, he cannot deal with quotient compositions (needed
for lifting theorems about @{text flat}. Also, a number of his definitions, like @{text ABS},
@{text REP} and @{text INJ} etc only exist in ML-code. On the other hand, Homeier
is able to deal with partial quotient constructions, which we have not implemented.
One advantage of our package is that it is modular---in the sense that every step
in the quotient construction can be done independently (see the criticism of Paulson
about other quotient packages). This modularity is essential in the context of
Isabelle, which supports type-classes and locales.
Another feature of our quotient package is that when lifting theorems, we can
precisely specify what the lifted theorem should look like. This feature is
necessary, for example, when lifting an inductive principle about two lists.
This principle has as the conclusion a predicate of the form @{text "P xs ys"},
and we can precisely specify whether we want to quotient @{text "xs"} or @{text "ys"},
or both. We found this feature very useful in the new version of Nominal
Isabelle.
\medskip
\noindent
{\bf Acknowledgements:} We would like to thank Peter Homeier for the
discussions about his HOL4 quotient package and explaining to us
some of its finer points in the implementation. Without his patient
help, this work would have been impossible.
*}
(*<*)
end
(*>*)