% This is quotient2.tex, the LaTeX2e file of the paper
% "Higher Order Quotients in Higher Order Logic"
% by Peter V. Homeier.
\documentclass[envcountsame,runningheads]{llncs}
\pagestyle{headings}
\setcounter{page}{1}

\usepackage{latexsym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{verbatim}
%

% ---------------------------------------------------------------------
% Resetting the margins.
% ---------------------------------------------------------------------
% \setlength{\topmargin}{0mm}
% \setlength{\headheight}{0mm}
% \setlength{\headsep}{0mm}
% \setlength{\oddsidemargin}{0mm}
% \setlength{\evensidemargin}{0mm}
% \setlength{\textheight}{9in}
% \setlength{\textwidth}{6.5in}

% ---------------------------------------------------------------------
% Input macros for importing EPS pictures.
% ---------------------------------------------------------------------
%\input boxedeps.tex %% obligatory (except for LaTeX, see below)
%\input boxedeps.cfg %% can replace next line:
%\SetOzTeXEPSFSpecial
%\ShowDisplacementBoxes %%alternatives \Hide \Show
%% \usepackage[oztex,hideboxes]{boxedeps}

% ---------------------------------------------------------------------
% Macro definitions.
% ---------------------------------------------------------------------
\def\fn{\hbox{$f\mkern-1.7mu n$}}
\def\vf{\hbox{$ch$}}
\def\ty#1{\hbox{$\hbox{\sl #1}$}}
\def\HOL{{\small HOL}}
\def\CCS{{\small CCS}}
\def\CSP{{\small CSP}}
\def\ML{{\small ML}}
\def\LCF{{\small LCF}}
\def\VCG{{\small VCG}}
\def\PPL{{\small PP}{\kern-.095em}$\lambda$}
\def\nul{\hbox{$\hbox{\bf 0}$}}
\def\ar#1#2#3{#1 \mathbin{\stackrel{\scriptstyle #2}{\longrightarrow}} #3}
\def\Rule#1#2{\mbox{${\displaystyle\raise 3pt\hbox{$\;\;#1\;\;$}} \over
	     {\displaystyle\lower5pt\hbox{$\;\;#2\;\;$}}$}}
%\def\defeq{{\overset{\mathrm{def}}=}}
\def\defeq{\stackrel{\mathrm{def}}{=}}

% ---------------------------------------------------------------------
% Macro for a tricky underbrace used later.
% ---------------------------------------------------------------------
\newbox\Tbox
\def\ud{\setbox\Tbox=\hbox{$\scriptstyle\rm name\; mapping$}%
  {\wd\Tbox=0mm\box\Tbox}}

% ---------------------------------------------------------------------
% Macros for a nice-looking `boxed figure'.
% ---------------------------------------------------------------------
\newlength{\rsize}
\setlength{\rsize}{0.3mm}
\newlength{\twidth}
\setlength{\twidth}{\textwidth}
\addtolength{\twidth}{-2\rsize}
\newbox\figbox
\long\def\Frame#1{\leavevmode
\hbox{\vbox{\hrule height\rsize
      \hbox{\vrule width\rsize #1\vrule width\rsize}
      \hrule height\rsize}}}
\def\fcaption#1{\refstepcounter{figure}\vbox{\vspace*{0mm}\hbox to\twidth{
	   \hfil
	   Figure \thefigure: #1 \hfil}\vspace*{0mm}}}
\def\caption#1{\refstepcounter{figure}\vbox{\vspace*{0mm}\hbox to\twidth{
	   \hfil
	   Table \thefigure: #1 \hfil}\vspace*{0mm}}}
%\def\fcaption#1{\refstepcounter{figure}\vbox{\vspace*{8mm}\hbox to\twidth{
%		   \hfil
%		   Figure \thefigure: #1 \hfil}\vspace*{5mm}}}
%\def\caption#1{\refstepcounter{figure}\vbox{\vspace*{8mm}\hbox to\twidth{
%		   \hfil
%		   Table \thefigure: #1 \hfil}\vspace*{5mm}}}


% -------------------------------
% New definitions for AMS symbols
% -------------------------------

%
\newcommand{\vb}{\;|\;\,}
\newcommand{\df}{\stackrel{\Delta}{=}}
\newcommand{\edoc}{\end{document}}
%
\newcommand{\lds}{\hspace*{0.2in}}
\newcommand{\ld}[1]{\noindent\hspace*{0.2in}$#1$}
\newcommand{\lfrac}[2]{\frac{{\textstyle #1}}{{\textstyle #2}}}
\newcommand{\lstk}[2]{\stackrel{{\textstyle #1}}{#2}}
\newcommand{\conequiv}{\mbox{${}^{xs} {\equiv} ^{ys}_{\alpha}$}}
\newcommand{\conequivn}{\mbox{${\rule{0mm}{1.8ex}}^{[\;]} {\equiv}^{[\;]}_{\alpha}$}}
\newcommand{\conequiva}[2]{\mbox{${}^{#1} {\equiv} ^{#2}_{\alpha}$}}
%\newcommand{\conequiva}[2]{\mbox{${\rule{0mm}{1.8ex}}^{#1} {\equiv} ^{#2}_{\alpha}$}}
\newcommand{\conequivv}[2]{\mbox{${}^{#1}_{\mathrm{var}} {\equiv} ^{#2}_{\alpha}$}}
%\newcommand{\preserves}[8]
%{\mbox{${#7} : {#5} \; {}^{#3}_{#1} {\equiv} ^{#4}_{#2} \; {#6} : {#8}$}}
%\newcommand{\preserves}[8]
%{\mbox{${#7} \leftarrow {#5} \; {}^{#3}_{#1} {\equiv} ^{#4}_{#2} \; {#6} \rightarrow {#8}$}}
\newcommand{\preserves}[8]
{\mbox{${#7} \succ {#5} \; {}^{#3}_{#1} {\equiv} ^{#4}_{#2} \; {#6} \prec {#8}$}}
\newcommand{\equiva}{{\equiv}_{\alpha}}
%\newcommand{\preservesa}[3] {\mbox{${#2} : \; {\equiv} \; {#1} : {#3}$}}
\newcommand{\refl}[1]{\mbox{$\stackrel{\scriptscriptstyle =}{#1}$}}
\newcommand{\itbf}[1]{\mbox{\itshape\bfseries{#1}}}
%\newcommand{\larrow}[0]{ \twoheadrightarrow_l }
%\newcommand{\larrow}[0]{\,\mbox{\makebox[0pt][l]{\hspace*{2.1mm}\raisebox{0.1mm}{$\shortparallel$}}$\longrightarrow$}\,}
\newcommand{\larrow}[0]{\mathbin{\mbox{\makebox[0pt][l]{\hspace*{0.7mm}\raisebox{0.14mm}{$\shortparallel$}}$\rightarrow$}}}
%
\newcommand{\varl}[1]{\mbox{${#1}$}}
\newcommand{\appl}[2]{\mbox{${#1}\;{#2}$}}
\newcommand{\laml}[2]{\mbox{$\lambda {#1}.\;{#2}$}}
\newcommand{\var}[1]{\mbox{${#1}$}}
\newcommand{\app}[2]{\mbox{${#1}\;{#2}$}}
\newcommand{\lam}[2]{\mbox{$\lambda {#1}.\;{#2}$}}
\newcommand{\presim}[0]{\mbox{$\mbox{\tt \$}\mathbin{\sim}$}}

% --------------------
% Symbols and keywords
% --------------------

\newcommand{\vvsub}{\mathrel{{//}_v}}
\newcommand{\mybigcup}{\mathop{\displaystyle\bigcup}\limits}
\newcommand{\mycross}{\mbox{$\;\times\;$}}
\newcommand{\mynot}{\mathop\sim}
\newcommand{\mydiv}{\mathrel{\bf div}}
%\newcommand{\cond}{\mbox{\tt \ => }}
%\newcommand{\alt}{\mbox{\tt \ | }}
\newcommand{\cond}{\mbox{\tt $\; => \;$}}
\newcommand{\alt}{\mbox{\tt $\; \mid \;$}}
%%\newcommand{\cond}{\mbox{\tt \; => \;}}
%%\newcommand{\alt}{\mbox{\tt \; | \;}}
\newcommand{\ldash}{\mbox{$\;$---$\;$}}
\newcommand{\append}{\mathbin{\&}}
\newcommand{\arrowx}{\mbox{$\;$---$\!\!\times\;$}}
\newcommand{\goal}{\mbox{?--}}
\newcommand{\Source}{\mbox{\sf Source}}
\newcommand{\Target}{\mbox{\sf Target}}
\newcommand{\Ssem}{\mbox{\sf Ssem}}
\newcommand{\Tsem}{\mbox{\sf Tsem}}
\newcommand{\goesto}[1]%
{\mbox{$\;\,\Longrightarrow_{\scriptscriptstyle #1}\,\;$}}
\newcommand{\pgoesto}[1]%
{\mbox{$\Longrightarrow_{\scriptscriptstyle #1}$}}
\newcommand{\myd}{\,\underline{\diamond}\,}
\newcommand{\like}[2]{\mbox{$#1\;\mbox{like}\;#2$}}
\newcommand{\lb}{\mbox{$[\![$}}
\newcommand{\rb}{\mbox{$]\!]$}}
\newcommand{\quotient}{partial equivalence}
\newcommand{\Quotient}{Partial Equivalence}
%\newcommand{\repofabs}{\mbox{\tt //}}
\newcommand{\repofabs}{\Downarrow}

% -------------------------
% Theorem environments
% -------------------------

%\newtheorem{atheorem}{Theorem}
%\newtheorem{alemma}[atheorem]{Lemma}
%\newtheorem{adefinition}[atheorem]{Definition}

% ---------------------------------------------------------------------
% Start of document
% ---------------------------------------------------------------------

\begin{document}


\title{Higher Order Quotients in Higher Order Logic}

\titlerunning{Higher Order Quotients in Higher Order Logic}

\author{Peter~V.~Homeier}

\authorrunning{Peter~V.~Homeier}

\institute{
U. S. Department of Defense
\\
palantir@trustworthytools.com
\\
http://www.trustworthytools.com
}

\maketitle

\begin{abstract}
The quotient operation is a standard feature of set theory, where
a set is partitioned into subsets by an equivalence relation.
% the resulting subsets of equivalent elements are called equivalence classes.
We reinterpret this idea for Higher Order Logic (HOL), where types are
divided by an equivalence relation to create new types, called
quotient types.
We present a tool for the Higher Order Logic theorem prover
to mechanically construct quotient types as
new types in the HOL logic,
and to automatically lift constants and
theorems about the original types
to corresponding constants and theorems about the quotient types.
%Tools are also provided to create quotients of aggregate types,
%in particular lists, pairs, sums, options, and function types.
This package exceeds the functionality of Harrison's package,
creating quotients of multiple mutually recursive types simultaneously,
and supporting the equivalence of aggregate types, such as lists and pairs.
Most importantly,
this package successfully
creates higher-order quotients, automatically lifting
theorems with quantification over functions
%on the quotient types
of any higher order.
% which to our knowledge has never been done before.
This is accomplished through the
%novel introduction
%key innovation
use
of {\it \quotient{} relations},
a possibly nonreflexive version of equivalence relations.
We demonstrate this tool by lifting Abadi and Cardelli's sigma calculus.
\end{abstract}


%
\section{Introduction}
%

The quotient operation is a standard feature of mathematics,
including set theory and abstract algebra.  It provides a way to
cleanly identify elements that previously were distinct.
This simplifies the system by removing unneeded structure.
%A system that discriminates between elements
%which are considered equivalent but not identical
%before the quotient operation thus gives rise to a system that identifies
%such equivalent elements so that they can no longer be distinguished.

Traditionally, quotients have found many applications.
Classic examples are the construction
of the integers from pairs of non-negative natural numbers,
or
%the construction of
the rationals from pairs of integers.
In the lambda calculus \cite{Bar81} and similar calculi, it is
common to identify terms which are alpha-equivalent, that differ only by
the choice of local names used by binding operators.
Other examples include the construction of bags from lists by ignoring order,
%where the order does not matter,
and the construction of sets from bags by ignoring duplicates.
%where if positive, the number of equal elements does not matter.

The ubiquity of quotients has recommended their investigation
%Since quotients are ubiquitous,
%they have been previously investigated
within the field of mechanical theorem proving.
The first to appear was Ton Kalker's 1989 package for HOL88 \cite{Kal89}.
Isabelle/HOL
\cite{NiPaWe02}
has mechanical support for the creation of
higher order quotients by Oscar Slotosch \cite{Slo97},
using partial equivalence relations represented as a type class,
with equivalence relations as a subclass.
That system provides a definitional framework for establishing
quotient types, including higher order.
Independently, Larry Paulson has shown a construction of first-order quotients
in Isabelle without any use of the Hilbert choice operator
\cite{LP04}.
PVS uses quotients to support theory interpretations \cite{OwS01}.
MetaPRL has quotients in its foundations,
as a type with a new equality \cite{Nog02}.
Coq, based on the Calculus of Constructions \cite{Hof95},
supports quotients \cite{GPWZ02} but
has some difficulties with higher order
\cite{CPS02}.
These systems provide little automatic support.
In particular, there is no automatic lifting of constants or theorems.

John Harrison has developed a package for the
%Higher Order Logic
HOL
theorem prover which supports first order quotients,
including automation to define new quotient types
%based on an existing type and an equivalence relation on that type,
and to lift to the quotient level both constants
and theorems previously established
\cite{Har98}.
%
This automatic lifting is key to practical support for quotients.
A quotient of a group
would be incomplete without also mapping the original group
operation to a corresponding one for the quotient group.
%Similarly, theorems about the group
%which are independent of the equivalence relation
Similarly, a theorem stating that the original group was abelian
should also be true of the quotient group.
%If one wished to take a quotient of a group, it would be inadequate to
%only create the quotient set of the original set by the equivalence relation,
%without appropriately mapping the original group operation to a corresponding
%group operation for the new quotient set.  Similarly, any theorems
%describing properties of the original group
%which are independent of the equivalence relation
%should also be true (in a translated form) of the new quotient group.
Mechanizing this lifting is vital for avoiding the repetition of proofs
at the higher level which were already proved at the lower level.
Such automation is not only practical, but mathematically incisive.
%Such automation makes the quotient operation more practical and intellectually cogent.

Despite the quality of Harrison's excellent package, it does have
limitations.  It can only lift one type at a time,
and does not deal with aggregate types, such as lists or pairs
involving types being lifted,
which makes it difficult to lift a family of mutually nested recursive types.
%Also, it does not deal with aggregate types, such as when some
%points of a mutual recursion involve the type operators (e.g., {\tt ('a)list}).
Most importantly, it is limited to lifting only first order theorems,
where
%universal and existential
quantification is permitted over the
type being lifted, but not over functions or predicates involving the type
being lifted.

In this paper we describe a new package for quotients for the Higher Order
Logic theorem prover that meets these three concerns.  It provides a tool
for lifting multiple types across multiple equivalence relations simultaneously.
Aggregate equivalence relations are produced and used automatically.
Most significantly, this package supports the automatic
lifting of theorems that involve higher order functions, including
quantification, of any finite order.
This is possible through the use of
{\it \quotient{} relations}
\cite{Rob89},
as a possibly non-reflexive variant of
equivalence relations, enabling
%the creation of
quotients
%relationships
of function types.
%rather than just simple or aggregate types.
%We introduce a new definition of when one type is a quotient of another,
%based on three properties that relate a \quotient{} relation to its
The relationship between these \quotient{} relations and their
associated abstraction and representation functions (mapping between the
lower and higher types)
is expressed in {\it quotient theorems\/} which
play a central and vital role in this package.

The precise definition of the quotient relationship between the
original and lifted types, and the proof of that relationship's
preservation
for a function type,
%given \quotient{} relations
given existing quotients
for the function's domain and range, are the heart of this paper,
and are presented in full detail.
These
%definition and proof
form the core theory that
justifies the treatment of all higher order functions,
including higher order
universal, existential, and unique existential quantification.

In addition, many existing polymorphic operators from the theories of
lists, pairs, sums, and options have theorems pre-proven
showing the operators' respectfulness of equivalence relations and
their preservation across quotients, yielding results at the
quotient level which correspond properly with their results at the lower level.
These respectfulness and preservation theorems enable the automatic
lifting of theorems that mention these operators.  Additional operators
can also be lifted by proving
and including
the corresponding respectfulness and preservation
theorems, which justify the operator's use across quotients.
%operations.

The system is thus extensible, both in terms of new operators, and even
in terms of new polymorphic type operators, by proving and including
theorems entailing
%the existence of
a quotient
of the type operator,
given quotients
of the
argument types.
%types which are arguments of the operator.

The structure of this paper is as follows.  In section \ref{quotientsets}
we briefly review quotient sets.  In section \ref{quotienttypes} we
re-interpret this idea for type theory.
Section \ref{equivalence} discusses equivalence relations and their
aggregates.
Section \ref{quotientrelation} describes \quotient{} relations,
their extension for aggregate and function types,
the properties of a quotient relationship,
and quotient extension theorems
for lifting aggregate and function types.
%%In particular,
%The quotient extension theorem for function types
%is the heart of higher order quotients, and
%%its proof is presented
%is proved
%in section \ref{condquotients}.
Section \ref{axiomofchoice} describes an alternative design
that avoids use of the Axiom of Choice.
Section \ref{liftingall} presents
the main tool of the quotient package, which lifts types, constants,
and theorems across the quotients.
The next several sections discuss
its work
%the work of the main tool of section \ref{liftingall}
in more detail.
Section \ref{newquotienttype}
describes the definition of new quotient types, and
section \ref{liftingdefs} describes the definition of lifted versions
of constants.
Section \ref{liftingtheorems} describes the various input theorems needed by
the tool to automatically lift theorems.
%from the lower level to the quotient level.
Section \ref{restrictions} describes the restrictions on theorems
in order for them to lift properly, and section
\ref{nonstandard} loosens these restrictions,
helpfully attempting to lift even some improper theorems.
%describing how the
%package will try to generate the proper theorem to lift
%even given an improper one.
%even if the given lower theorem is not proper.
Section \ref{liftingsets} discusses lifting theorems about sets.
In sections \ref{sigmacalculus} through
\ref{puresigmacalculus}, we present Abadi and Cardelli's sigma calculus
\cite{AbCa96},
its formulation in HOL and its lifting by quotients over alpha-equivalence.
Finally, our conclusions are presented in section \ref{conclusions}.

We are grateful for the helpful comments and
suggestions made by
Rob Arthan,
Randolph Johnson,
Sylvan Pinsky,
Yvonne V. Shashoua,
and
Konrad Slind,
%which have greatly improved this paper.
and especially Michael Mislove for identifying
partial equivalence relations and
William Schneeberger for the key idea in the proof of theorem
\ref{partinverses}.


%
\section{Quotient Sets}
%
\label{quotientsets}

Quotient sets are a standard construction of set theory.
They have found wide application in many areas of mathematics,
including algebra and logic.
The following description is abstracted from \cite{End77}.

A binary relation
$\sim$
on $S$ is
an {\it equivalence relation\/}
if it is reflexive, symmetric,  and transitive.
$$
\begin{array}{l@{\hspace{0.6cm}}l@{\hspace{0.3cm}}l}
\mbox{\it reflexive:} &
\forall x \in S. & x \sim x \\
\mbox{\it symmetric:} &
\forall x,y \in S. & x \sim y \ \Rightarrow \ y \sim x \\
\mbox{\it transitive:} &
\forall x,y,z \in S. & x \sim y \ \wedge \ y \sim z \ \Rightarrow \ x \sim z
\end{array}
$$
Let $\sim$ be an equivalence relation.
Then the {\it equivalence class\/} of $x$ ({\it modulo\/} $\sim$)
is defined as $[ x ]_{\sim} \defeq \{ y \ | \ x \sim y \}$.
It follows \cite{End77} that
$$
[ x ]_{\sim} = [ y ]_{\sim} \ \ \Leftrightarrow \ \ x \sim y .
$$

\noindent
The {\it quotient set\/} $S / \mathbin{\sim}$ is defined as
%is defined as the set of equivalence classes of elements of $S$.
$$
S / \mathbin{\sim} \ \defeq \ \{ [ x ]_{\sim} \ | \ x \in S \}.
$$
\noindent
This is the set of all equivalence classes modulo $\sim$ of elements in $S$.

%A {\it partition\/} $\Pi$ of a set $S$ is a set of nonempty subsets of $S$
%that is disjoint and exhaustive.
%Then
%$S / \mathbin{\sim}$ is a partition of $S$
%\cite{End77}.


%
\section{Equivalence Relations and Equivalence Theorems}
%
\label{equivalence}

%Quotient sets \cite{End77} are a standard construction of set theory.
%%They have found wide application in many areas of mathematics,
%%including algebra and logic.
%
%We reinterpret quotient sets
%\cite{End77}
%for the Higher Order Logic theorem prover
%\cite{GoMe93},
%whose logic is a type theory, rather than a set theory.
%
Before considering quotients, we examine equivalence relations,
on which such traditional quotients as those mentioned in the introduction
have been based.

Let $\tau$ be any type.  A binary relation $R$ on $\tau$ can be
represented in HOL as a curried function
of type $\tau \rightarrow (\tau \rightarrow \mbox{\tt bool})$.
We will take advantage of the curried nature of $R$, where
$R\ x\ y = (R\ x)\ y$.

An equivalence relation is a binary relation $E$ satisfying
$$
\begin{array}{l@{\hspace{0.6cm}}l@{\hspace{0.3cm}}l}
\mbox{\it reflexivity:} &
\forall x:\tau . & E\ x\ x \\
\mbox{\it symmetry:} &
\forall x\ y :\tau. & E\ x\ y \ \Rightarrow \ E\ y\ x \\
\mbox{\it transitivity:} &
\forall x\ y\ z:\tau. & E\ x\ y \ \wedge \ E\ y\ z \ \Rightarrow \ E\ x\ z
\end{array}
$$

These three properties are encompassed in
%one, which we call
the {\it equivalence property:}
$$
%\begin{array}[t]{l@{\hspace{0.5cm}}l@{\hspace{1.5cm}}}
\begin{array}[t]{l@{\hspace{0.6cm}}l@{\hspace{0.3cm}}}
\mbox{\it equivalence:} &
\mbox{\tt EQUIV}\ E \ \defeq \
\forall x\ y :\tau.\ E\ x\ y \ \Leftrightarrow \ (E\ x = E\ y)
\end{array}
$$

\noindent
A theorem of the form
$\vdash$ {\tt EQUIV} $E$
%($E : \tau$ {\tt ->} $\tau$ {\tt -> bool})
is called an {\it equivalence theorem\/} on type $\tau$.

Given an equivalence theorem, we can obtain the reflexive, symmetric,
and transitive properties, or given those three, construct the corresponding
equivalence theorem, using the following Standard ML functions of our package.
\begin{center}
\framebox{
\begin{tabular}[t]{rl}
{\tt equiv\_refl} & {\tt : thm -> thm} \\
{\tt equiv\_sym} & {\tt : thm -> thm} \\
{\tt equiv\_trans} & {\tt : thm -> thm}  \\
{\tt refl\_sym\_trans\_equiv} & {\tt : thm -> thm -> thm -> thm}  \\
\end{tabular}
}
\end{center}

%
\subsection{Equivalence Extension Theorems}
%
\label{condequivs}

Given an equivalence relation
%{\it E\/}{\tt :ty} $\rightarrow$ {\tt ty} $\rightarrow$ {\tt bool}
$E:\tau \rightarrow \tau \rightarrow \mbox{\tt bool}$
on values of type $\tau$,
there is a natural extension of {\it E\/} to values of lists of $\tau$.
This is expressed as {\tt LIST\_REL\;{\it E\/}},
which forms an equivalence relation of type
%{\tt (ty)list} $\rightarrow$ {\tt (ty)list} $\rightarrow$ {\tt bool}.
$\tau\ \mbox{\tt list} \rightarrow \tau\ \mbox{\tt list} \rightarrow \mbox{\tt bool}$.
Similarly, equivalence relations on pairs, sums, and options
may be formed
%in the HOL logic
from their constituent types' equivalence relations by the following operators.

\begin{center}
\framebox{
\begin{tabular}[t]{lrl}
Type & Operator \ \ \ \ \ & Type of operator \\
\hline \\
%identity & {\tt = : } & {\tt 'a -> 'a -> bool} \\
list & {\tt LIST\_REL : } & {\tt ('a -> 'a -> bool) ->} \\
& & {\tt \ \ \ \ \ \ 'a list -> 'a list -> bool} \\
pair & {\tt \#\#\# : } & {\tt ('a -> 'a -> bool) -> ('b -> 'b -> bool) ->} \\
& & {\tt \ \ \ \ \ \ 'a \# 'b -> 'a \# 'b -> bool}  \\
sum & {\tt +++ : } & {\tt ('a -> 'a -> bool) -> ('b -> 'b -> bool) ->} \\
& & {\tt \ \ \ \ \ \ 'a + 'b -> 'a + 'b -> bool}  \\
option\ \ & {\tt OPTION\_REL : } & {\tt ('a -> 'a -> bool) ->} \\
& & {\tt \ \ \ \ \ \ 'a option -> 'a option -> bool}  \\
% fun & {\tt ===> : } & {\tt ('a -> 'a -> bool) -> ('b -> 'b -> bool) ->} \\
% & & {\tt \ \ \ \ \ \ ('a -> 'b) -> ('a -> 'b) -> bool}  \\
\end{tabular}
}
\end{center}

These operators are defined
as indicated below.

\begin{definition}
\label{listrel}
$\begin{array}[t]{lcccl}
\mbox{\tt LIST\_REL}\ R & \mbox{\tt []} & \mbox{\tt []} & \ = \  & \mbox{\bf true} \\
\mbox{\tt LIST\_REL}\ R & (a \mbox{\tt ::} as) & \mbox{\tt []} & \ = \ & \mbox{\bf false}\\
\mbox{\tt LIST\_REL}\ R & \mbox{\tt []} & (b \mbox{\tt ::} bs) & \ = \  & \mbox{\bf false}\\
\mbox{\tt LIST\_REL}\ R & (a \mbox{\tt ::} as) & (b \mbox{\tt ::} bs) & \ = \
   & R\ a\ b\ \wedge \mbox{\tt LIST\_REL}\ R\ as\ bs
\end{array}$
\end{definition}

\begin{definition}
\label{pairrel}
$\begin{array}[t]{lcccl}
(R_1\ \mbox{\tt \#\#\#}\ R_2) & (a_1, a_2) & (b_1, b_2) & \ = \
   & R_1\ a_1\ b_1 \ \wedge \ R_2\ a_2\ b_2
\end{array}$
\end{definition}

\begin{definition}
\label{sumrel}
$\begin{array}[t]{lcccl}
(R_1\ \mbox{\tt +++}\ R_2) & (\mbox{\tt INL}\ a_1) & (\mbox{\tt INL}\ b_1) & \ = \
   & R_1\ a_1\ b_1  \\
(R_1\ \mbox{\tt +++}\ R_2) & (\mbox{\tt INL}\ a_1) & (\mbox{\tt INR}\ b_2) & \ = \
   & \mbox{\bf false}  \\
(R_1\ \mbox{\tt +++}\ R_2) & (\mbox{\tt INR}\ a_2) & (\mbox{\tt INL}\ b_1) & \ = \
   & \mbox{\bf false}  \\
(R_1\ \mbox{\tt +++}\ R_2) & (\mbox{\tt INR}\ a_2) & (\mbox{\tt INR}\ b_2) & \ = \
   & R_2\ a_2\ b_2
\end{array}$
\end{definition}

\begin{definition}
\label{optionrel}
$\begin{array}[t]{lcccl}
\mbox{\tt OPTION\_REL}\ R & \mbox{\tt NONE} & \mbox{\tt NONE} & \ = \
   & \mbox{\bf true}  \\
\mbox{\tt OPTION\_REL}\ R & (\mbox{\tt SOME}\ a) & \mbox{\tt NONE} & \ = \
   & \mbox{\bf false}  \\
\mbox{\tt OPTION\_REL}\ R & \mbox{\tt NONE} & (\mbox{\tt SOME}\ b) & \ = \
   & \mbox{\bf false}  \\
\mbox{\tt OPTION\_REL}\ R & (\mbox{\tt SOME}\ a) & (\mbox{\tt SOME}\ b) & \ = \
   & R\ a\ b
\end{array}$
\end{definition}

They
%operators
take
%one or two
arguments which are the
equivalence relations for component subtypes, and return
an equivalence relation for the aggregate type.

Since the pair and sum relation operators have two arguments,
they are infix, whereas the list and option relation operators
are unary, prefix operators.
The operator definitions
may be needed to prove respectfulness
(see \S \ref{respectfulness}, \ref{polyrespects}).

Given equivalence theorems for the constituent subtypes, the
equivalence theorems for the natural extensions to aggregate types (e.g.,
lists, pairs, sums, and options) may be created by the following
SML functions of our package.

\begin{center}
\framebox{
\begin{tabular}[t]{rl}
{\tt list\_equiv} & {\tt : thm -> thm} \\
{\tt pair\_equiv} & {\tt : thm -> thm -> thm} \\
{\tt sum\_equiv} & {\tt : thm -> thm -> thm}  \\
{\tt option\_equiv} & {\tt : thm -> thm}  \\
\\
{\tt identity\_equiv} & {\tt : hol\_type -> thm}  \\
{\tt make\_equiv} & {\tt : thm list -> hol\_type -> thm}  \\
\end{tabular}
}
\end{center}

{\tt identity\_equiv} {\it ty\/} creates the trivial equivalence theorem for
the given type {\it ty,} using equality ({\tt =}) as the equivalence relation.

{\tt make\_equiv} {\it equivs ty\/} creates an equivalence
theorem for the given type {\it ty,}
which may be a complex type expression with lists, pairs, etc.
Here {\it equivs} is a list of both equivalence theorems
for the base types and equivalence extension theorems for type operators
(see section \ref{condequivs}).

{\it Equivalence extension theorems\/} for type operators
%as:
have the form:
\begin{center}
\begin{tabular}{rl}
$\vdash$ & {\tt $\forall$E1 ... En. }  \\
& {\tt ($\forall$(x:$\alpha_1$) (y:$\alpha_1$). E1 x y $\Leftrightarrow$ (E1 x = E1 y)) $\Rightarrow$}
% \\
%& {\tt ...} \\
 {\tt ...} \\
& {\tt ($\forall$(x:$\alpha_n$) (y:$\alpha_n$). En x y $\Leftrightarrow$ (En x = En y)) $\Rightarrow$}  \\
& {\tt ($\forall$(x:$(\alpha_1,...,\alpha_n)op$) (y:$(\alpha_1,...,\alpha_n)op$).}  \\
& \hspace{4mm}
{\tt OP\_REL E1 ... En x y $\Leftrightarrow$ }  \\
& {\tt
\hspace{5mm}
(OP\_REL E1 ... En x = OP\_REL E1 ... En y))}  \\
\end{tabular}
\end{center}

Given the type operator $(\alpha_1,...,\alpha_n)op$,
{\tt OP\_REL} should be an operator which takes $n$ arguments,
which are the equivalence relations {\tt E1} through {\tt En}
on the types $\alpha_1$ through $\alpha_n$,
%and yields
yielding
an equivalence relation for the type $(\alpha_1,...,\alpha_n)op$.

Using the above relation extension operators,
the aggregate type operators {\tt list},
{\tt prod},
{\tt sum}, and
{\tt option}
%{\tt ($\alpha$)list},
%{\tt ($\alpha$)option},
%{\tt ($\alpha,\beta$)prod}, and
%{\tt ($\alpha,\beta$)sum}
have the following equivalence extension theorems:

\vspace{3mm}

\noindent
{\tt
\begin{tabular}{ll}
LIST\_EQUIV: &
 $\vdash \forall E.\ \mbox{\tt EQUIV}\ E  \;\Rightarrow \;\mbox{\tt EQUIV}\;(\mbox{\tt LIST\_REL}\ E)$ \\
%\\
PAIR\_EQUIV: &
 $\vdash \forall E_1\ E_2.\ \mbox{\tt EQUIV}\ E_1  \;\Rightarrow \;
                            \mbox{\tt EQUIV}\ E_2  \;\Rightarrow \;
         \mbox{\tt EQUIV}\;(E_1\ \mbox{\tt \#\#\#}\ E_2)$ \\
% $\vdash \forall E_1\ E_2.$  EQUIV $E_1$  $\Rightarrow$ EQUIV $E_2$ $\Rightarrow$
%                        EQUIV\;($E_1$ \#\#\# $E_2$) \\
%\\
SUM\_EQUIV: \  &
 $\vdash \forall E_1\ E_2.\ \mbox{\tt EQUIV}\ E_1  \;\Rightarrow \;
                            \mbox{\tt EQUIV}\ E_2  \;\Rightarrow \;
         \mbox{\tt EQUIV}\;(E_1\ \mbox{\tt +++}\ E_2)$ \\
% $\vdash \forall E_1\ E_2.$  EQUIV $E_1$  $\Rightarrow$ EQUIV $E_2$ $\Rightarrow$
%                        EQUIV\;($E_1$ +++ $E_2$) \\
%\\
OPTION\_EQUIV: &
 $\vdash \forall E.\ \mbox{\tt EQUIV}\ E  \;\Rightarrow \;\mbox{\tt EQUIV}\;(\mbox{\tt OPTION\_REL}\ E)$ \\
% $\vdash \forall E$.  EQUIV $E$  $\Rightarrow$ EQUIV\;(OPTION\_REL $E$) \\
\end{tabular}
}


%
\section{Partial Equivalence Relations and Quotient Theorems}
%
\label{quotientrelation}

In this section we introduce a new definition of the quotient
relationship, based on {\it \quotient{} relations}
(PERs), related to but different from equivalence relations.
%a related but different concept than equivalence relations.
Every equivalence relation is a \quotient{} relation, but
not every \quotient{} relation is an equivalence relation.
An equivalence relation is reflexive, symmetric and transitive,
while a \quotient{} relation is symmetric and transitive, but not
necessarily reflexive on all of its domain.

Why use \quotient{} relations with a weaker reflexivity condition?
The reason involves forming quotients of higher order types, that is,
functions whose domains or ranges involve types being lifted.  Unlike lists
and pairs, the equivalence relations for the domain and range do not
naturally extend to a useful equivalence relation for functions
from the domain to the range.

The reason is that not all functions which are elements of the function
type are {\it respectful\/} of the associated equivalence relations,
as described in
section {\ref{respectfulness}}.
For example, given an equivalence relation
$E:\tau \rightarrow \tau \rightarrow \mbox{\tt bool}$,
the set of functions from $\tau$ to $\tau$ may contain a function
$f^?$ where for some $x$ and $y$
%of type $\tau$
which are equivalent
($E\ x\ y$), the results of $f^?$ are not equivalent
($\neg (E\ (f^?\ x)\ (f^?\ y))$).
Such disrespectful functions cannot be worked with; they do not
correspond to any function at the abstract quotient level.
%
Suppose instead that $f^?$ did lift.
Let $\lceil \phi \rceil$ be the lifted version of $\phi$.
As $\lceil f^? \rceil$ is the lifted version of $f^?$,
it should act just like $f^?$ on its argument,
except that it should not consider the lower level details
that $E$
%and thus $\lceil \_ \rceil$
disregards.
%collapses.
%obscures.
Thus
%Because we assume that $f^?$ lifts,
$
\forall u.\
\lceil f^? \rceil \lceil u \rceil =
\lceil f^?\ u \rceil $.
%This means that the lifted version of $f^?$ must act on lifted versions
%of its argument just as if the original $f^?$ had been applied to the
%original argument, and the result lifted.
Then
certainly
$\forall u\ v.\ E\ u\ v \Leftrightarrow (\lceil u \rceil = \lceil v \rceil)$,
and
because $E\ x\ y$, we must have $\lceil x \rceil = \lceil y \rceil$.
Applying $\lceil f^? \rceil$ to both sides,
$\lceil f^? \rceil \lceil x \rceil = \lceil f^? \rceil \lceil y \rceil$.
But this implies $\lceil f^?\ x \rceil = \lceil f^?\ y \rceil$,
which means that $E\ (f^?\ x)\ (f^?\ y)$, which we have said is false,
a contradiction.
%
\begin{comment}
%Every theorem at the quotient level should correspond to a theorem at
%the lower level.
Any equivalence relation $E^2$ for the function type
$\tau \rightarrow \tau$
would
have to be reflexive, so we would have $E^2\ f^?\ f^?$.
%which with $E\ x\ y$ would {\it not\/} imply $E (f^? x) (f^? y)$.
But this would invalidate
%{\tt ?- \verb+~+(?f1 f2 x. $E^2$ f1 f2 $\wedge$ \verb+~+$E$ (f1 x) (f2 x)},
%{\tt ?- !f1 f2 x. $E^2$ f1 f2 $\Rightarrow$ $E$ (f1 x) (f2 x)}
%(take ${\tt f1}\ z = f^? x$, and ${\tt f2}\ z = f^? y$),
%$\forall f_1 f_2\ x.\ E^2 f_1 f_2 \Rightarrow E (f_1\ x) (f_2\ x)$
%$\forall f_1 f_2\ x\ y.\ E^2 f_1 f_2 \wedge E\ x\ y \Rightarrow
%$\forall f_1\, f_2\, x\,y.\ E^2 f_1 f_2 \wedge E\ x\ y \Rightarrow E (f_1\ x) (f_2\ y)$,
%$\forall f, g, x, y.\ E^2 f g \wedge E\ x\ y \Rightarrow E (f\ x) (g\ y)$,
%$\forall f_1, f_2, x, y.\ E^2 f_1 f_2 \wedge E\ x\ y \Rightarrow E (f_1\ x) (f_2\ y)$,
$\forall f_1\;f_2\;x\;y.\; E^2 f_1\:f_2 \wedge E\ x\ y \Rightarrow E (f_1\;x) (f_2\;y)$,
%the lower unlifted version of
%to be lifted to
the higher version of which is
%the true
%{\tt |- \verb+~+(?f1 f2 x. f1 = f2 $\wedge$ \verb+~+(f1 x = f2 x)},
%{\tt |- !f1 f2 x. f1 = f2 $\Rightarrow$ (f1 x = f2 x)},
%$\forall f_1 f_2\ x.\ (f_1 = f_2) \Rightarrow (f_1\ x = f_2\ x)$,
%$\forall f_1 f_2\ x\ y.\ (f_1 = f_2) \wedge (x = y) \Rightarrow (f_1\ x = f_2\ y)$,
%$\forall f_1, f_2, x, y.\ (f_1 = f_2) \wedge (x = y) \Rightarrow (f_1\ x = f_2\ y)$,
%$\forall f_1\,f_2\, x\,y.\ f_1 = f_2 \wedge x = y \Rightarrow f_1\ x = f_2\ y$,
%$\forall f, g, x, y.\ f = g \wedge x = y \Rightarrow f\ x = g\ y$,
%$\forall f_1, f_2, x, y.\ f_1 = f_2 \wedge x = y \Rightarrow f_1\ x = f_2\ y$,
$\forall f_1\;f_2\;x\;y.\;f_1 = f_2 \wedge x = y \Rightarrow f_1\;x = f_2\;y$,
which is obviously true.
%Every theorem at the higher level should correspond to a theorem at the lower level.
%Every provable statement at the higher level should translate to a provable one at the lower level.
Just as every element of the higher type should translate to at least one
element at the lower level,
every true statement at the higher level should translate to a true statement at the lower level.
But this principle is violated in this case.
\end{comment}
Therefore such disrespectful functions cannot be lifted, and
we must exclude them.  Using \quotient{} relations
accomplishes this exclusion.
%Therefore we exclude such disrespectful functions
%Ordinary function application would be intractable.
%Therefore such disrespectful functions should be excluded
%from relations between functions.
%Hence a \quotient{} relation
%cannot be fully reflexive if its domain is a function type.
\begin{comment}
The resulting
%\quotient{}
relation cannot be
a true equivalence,
%an equivalence,
%an equivalence relation,
but it could be described as an equivalence relation on the field of
the relation, the field being the set of elements which
are related to any element.
\end{comment}

First, we say an element $r$ {\it respects R\/} if and only if
{\it R\/} {\it r\/} {\it r}.

\begin{definition}[Quotient]
\label{quotientdef}
%We define that
A relation {\it R\/}
with
%is a {\it \quotient{} relation\/} with respect to
abstraction function {\it abs\/}
and representation function {\it rep\/}
(between the representation, lower type $\tau$
and the abstract, quotient type $\xi$)
is a {\it quotient}
(notated as $\langle R$,${\it abs}$,${\it rep} \rangle$)
if and only if
%the following hold:
\end{definition}

\begin{center}
\begin{tabular}[t]{l@{\hspace{0.5cm}}l}
%{\it rep is right inverse of abs}
(1)
& $\forall a:\xi.$ {\it abs} ({\it rep} $a$) = $a$ \\
%{\it reflexivity of rep}
(2)
& $\forall a:\xi.$ {\it R\/} ({\it rep} $a$) ({\it rep} $a$) \\
%{\it proper equivalence}
(3)
& $\forall r,s:\tau.$
{\it R\/} $r$ $s$ $\Leftrightarrow$
{\it R\/} $r$ $r$ $\wedge$
{\it R\/} $s$ $s$ $\wedge$
({\it abs} $r$ = {\it abs} $s$) \\
\end{tabular}
\end{center}

Property 1 states that {\it rep\/} is a right inverse of {\it abs}.

Property 2 states that
%{\it R\/} is reflexive on the range of {\it rep}.
the range of {\it rep} respects {\it R}.

Property 3 states that two elements of $\tau$ are related by {\it R\/}
if and only if
each element respects {\it R} and their abstractions are equal.

%Of course, if {\it R\/} is an equivalence relation, then for example
%it is reflexive on all elements, not only the range of {\it rep}
%(property 2).
%But the properties here describe a
%{\it \quotient{} relation}, which is not the same as an equivalence relation.

%These properties imply that {\it R\/} is a \quotient{} relation.

These three properties (1-3) describe the way
the \quotient{} relation {\it R\/} works together with
{\it abs\/} and {\it rep}
to establish the correct
quotient relationship between the lower type $\tau$
and the quotient type $\xi$.
The precise definition of this quotient relationship
is a central contribution of this work.
%This relationship is so important that we give it a special definition:
This relationship is defined in the HOL logic as a new predicate:
{\tt
\begin{tabbing}
\hspace{3.5mm}
  QUOTI\=ENT  (R:'a -> 'a -> bool) (abs:'a -> 'b) (rep:'b -> 'a) $\Leftrightarrow$ \\
\>       ($\forall$a. abs (rep a) = a) $\wedge$ \\
\>       ($\forall$a. R (rep a) (rep a)) $\wedge$ \\
\>       ($\forall$r s. R r s $\Leftrightarrow$ R r r $\wedge$ R s s $\wedge$ (abs r = abs s))
\end{tabbing}}

\noindent
The relationship that {\it R\/} with {\it abs\/} and {\it rep\/}
is a quotient is
%concisely notated as $\langle R$,${\it abs}$,${\it rep} \rangle$, or
expressed in HOL as
\begin{center}
\tt
$\vdash$ QUOTIENT {\it R\/} {\it abs\/} {\it rep} .
\end{center}

\noindent
A theorem of this form is called a {\it quotient theorem}.
The identity is
$\vdash \langle \mbox{\tt \$=}, \mbox{\tt I}, \mbox{\tt I} \rangle$.
%They play a central role within this quotient package.

\begin{comment}
The traditional construction requires the elements of the
%new
quotient
type to be subsets of the original type.
This definition of quotients only requires them to be isomorphic.
\end{comment}
%
%The above definition is a fundamental revision of the notion of quotients.
%As will be shown in section \ref{condquotients},
These three properties support the inference of a quotient theorem for a
function type, given quotient theorems for the domain and the range.
This key inference is central and necessary to enable higher order quotients.


%
\section{Quotient Types}
%
\label{quotienttypes}

The user may specify a quotient of a type $\tau$ by a relation $R$
(written $\tau / R$) by giving
either a theorem that the relation is an equivalence relation, of the form
\begin{equation}
\vdash
\forall x\ y.\ R\ x\ y \ \Leftrightarrow \ (R\ x = R\ y) \ ,
\end{equation}
or one
%by giving a theorem
that the relation is a nonempty partial equivalence relation, of the form
\begin{equation}
\label{PERinput}
\vdash
(\exists x.\ R\ x\ x) \ \wedge \
(\forall x\ y.\ R\ x\ y \ \Leftrightarrow \
                R\ x\ x \wedge R\ y\ y \wedge (R\ x = R\ y)) \ .
\end{equation}

%
Alternatively, these theorems may be equivalently expressed as
$\vdash \mbox{\tt EQUIV}\ R$ or
$\vdash \mbox{\tt PARTIAL\_EQUIV}\ R$, respectively,
%These abbreviations are
defined in
%the theorems
{\tt EQUIV\_def}
and {\tt PARTIAL\_EQUIV\_def}.
In this section we will develop the second, more difficult case (2).
The first follows immediately.
%, where the theorem describes a nonempty partial equivalence relation.
In the following, $x$, $y$, $r$, $s : \tau$, $c : \tau\rightarrow{\tt bool}$,
and $a : \tau / R$.

New types may be defined in HOL
using the function {\tt new\_type\_definition}
%and {\tt define\_new\_type\_bijections}
\cite[sections 18.2.2.3-5]{GoMe93}.
This function requires us to
%To define a new type in higher order logic, we must
choose a representing
type, and a predicate on that type denoting a subset that is nonempty.

\begin{definition}
\label{quotient_type_def}
We define the new
{\it quotient type\/} $\tau / R$
%\mathbin{\sim}$
as isomorphic to the subset of
%by
the representing type $\tau \rightarrow \mbox{\tt bool}$
%and
%selected
by the
predicate $P : (\tau \rightarrow \mbox{\tt bool}) \rightarrow \mbox{\tt bool}$,
where
$
P \ c \ \defeq \ \exists x.\ R\ x\ x \wedge (c = R\ x).
$
\end{definition}

\noindent
{\it P\/} is nonempty because $P\ (R\ x)$ for the $x$\,:\,$\tau$
such that $R\ x\ x$ by (\ref{PERinput}).
Let $\xi = \tau / R$.
The HOL tool
{\tt define\_new\_type\_bijections}
\cite{GoMe93} automatically defines
%in the HOL logic
%an abstraction
%function $\lceil \_ \rceil_c
%: (\tau \rightarrow \mbox{\tt bool}) \rightarrow  \xi$
%and a representation function $\lfloor \_ \rfloor_c
%: \xi \rightarrow (\tau \rightarrow \mbox{\tt bool}) $, such that
%abstraction and representation functions
a function
%$\lceil \_ \rceil_c
$\mbox{\it abs}_c :(\tau \rightarrow \mbox{\tt bool}) \rightarrow  \xi$
and its right inverse
%$\lfloor \_ \rfloor_c
$\mbox{\it rep}_c :\xi \rightarrow (\tau \rightarrow \mbox{\tt bool}) $ satisfying

\begin{definition}
\label{abs_rep_classes}
$
%(\forall a:\xi.\ \lceil \, \lfloor a \rfloor_c \rceil_c = a)
%\ \wedge \
%(\forall f:\tau \rightarrow \mbox{\tt bool}.\
%P\ f \, \Leftrightarrow (\lfloor \, \lceil f \rceil_c \rfloor_c = f)) .
\begin{array}[t]{ll}
(\mbox{\rm a})\ & \forall a:\xi.\ {\it abs}_c \ ({\it rep}_c \ a) = a
%\ \wedge
\\
(\mbox{\rm b}) & \forall c:\tau \rightarrow \mbox{\tt bool}.\
P\ c
%(\exists x.\ R\ x\ x \wedge (c = R\ x))
\ \Leftrightarrow \ {\it rep}_c \ ({\it abs}_c \ c) = c
\end{array}
$
\end{definition}

\noindent
%{\it``PER classes''}
{\it PER classes\/}
are subsets of $\tau$ (of type $\tau \rightarrow \mbox{\tt bool}$)
which satisfy $P$.
Then ${\it abs}_c$ and ${\it rep}_c$
map between
the quotient type $\xi$
and
PER classes (hence the ``$c$'').

%\noindent
%and returns Definition \ref{abs_rep_classes} as its result.
%These functions are used to create identifiable values of the new type.
%and to establish their interrelationships.
%(The `${}_c$' is notation.)
%
%For the $P$ of Definition \ref{quotient_type_def}, we can prove:
%\begin{theorem}
%\label{abs_rep_classes_simple}
%$
%(\forall a
%%:\xi
%.\ \lceil \, \lfloor a \rfloor_c \rceil_c = a)
%\ \wedge \
%(\forall f.\ (\exists x.\ R\ x\ x \wedge f = R\ x) \Leftrightarrow
%\lfloor \, \lceil \, f  \rceil_c \rfloor_c = f ) .
%$
%\end{theorem}
%Proof:
%The left conjunct comes directly from Definition \ref{abs_rep_classes}.
%Also by that theorem, the right conjunct is equivalent to
%$\forall r.\ P\ [ r ]_E$.
%% !r. (\c. ?r. c = ALPHA r) (ALPHA r)
%Then
%$
%P\ [ r ]_E =
%%P\ (E\ r) =
%(\exists x.\ [ r ]_E = [ x ]_E)
%$
%which is proven true by choosing the witness $x = r$.
%$\Box$

\begin{lemma}[${\it rep}_c$ maps to PER classes]
\label{ty_REP_REL}
$\forall a.\
P\ ({\it rep}_c\ a)$.
%\exists r.\ R\ r\ r\ \wedge \ {\it rep}_c\ a = R\ r$.
\end{lemma}
Proof:
By
%the first clause of
Definition \ref{abs_rep_classes}(a),
$ {\it abs}_c\ ({\it rep}_c\ a) = a$, so taking
the ${\it rep}_c$ of both sides,
$ {\it rep}_c\ ({\it abs}_c\ ({\it rep}_c\ a)) = {\it rep}_c\ a$.
By
%the second clause of
Definition \ref{abs_rep_classes}(b),
%this implies
$P\ ({\it rep}_c\ a)$.
%By the definition of $P$, this is
%the goal.
$\Box$

%\begin{corollary}
%\label{ty_REP_REL_cor}
%$\forall a.\
%\exists r.\
%R\ r\ r\ \wedge\ {\it rep}_c\ a = R\ r$.
%%{\it rep}_c\ ({\it abs}_c\ ({\it rep}_c\ a)) = {\it rep}_c\ a$.
%\end{corollary}

\begin{lemma}
\label{ty_REP_ABS}
$\forall r.\
R\ r\ r \Rightarrow
({\it rep}_c\ ({\it abs}_c\ (R\ r)) = R\ r)$.
\end{lemma}
Proof: Assume $R\ r\ r$; then $P\ (R\ r)$.
By Definition \ref{abs_rep_classes}(b), the goal follows.

\begin{lemma}[${\it abs}_c$ is one-to-one on PER classes]
\label{ty_ABS_11}
\\
$\forall r\ s.\
R\ r\ r \Rightarrow
R\ s\ s \Rightarrow
({\it abs}_c\ (R\ r) = {\it abs}_c\ (R\ s)
\ \Leftrightarrow \ R\ r = R\ s)$.
\end{lemma}
Proof:  Assume $R\ r\ r$ and $R\ s\ s$.
%Then $P\ (R\ r)$ and $P\ (R\ s)$
%by the definition of $P$.
The right-to-left implication of the biconditional is trivial.
Assume ${\it abs}_c\ (R\ x) = {\it abs}_c\ (R\ y)$.
Applying ${\it rep}_c$ to
both sides gives us
${\it rep}_c\ ({\it abs}_c\ (R\ x)) = {\it rep}_c\ ({\it abs}_c\ (R\ y))$.
%By Lemma \ref{ty_REP_REL}, $P$ is true of both sides.
%$P\ ({\it rep}_c\ ({\it abs}_c (R\ x))$.
Then by
%Definition \ref{abs_rep_classes}(b),
Lemma \ref{ty_REP_ABS} twice,
$R\ x = R\ y$.
$\Box$

\vspace{\topsep}
The functions
${\it abs}_c$ and ${\it rep}_c$
map between PER classes of type
$\tau \rightarrow \mbox{\tt bool}$ and the quotient type $\xi$.
Using these functions, we can define new functions
${\it abs}$ and ${\it rep}$
between the original
type $\tau$ and the quotient type $\xi$ as follows.
\begin{definition}[Quotient abstraction and representation functions]
\label{abs_rep_def}
$$
\begin{array}[t]{c@{\hspace{0.1cm}}c@{\hspace{0.1cm}}l@{\hspace{1.0cm}}rcl}
{\it abs} & : & \tau \rightarrow \xi &
{\it abs}\ r & \ \defeq \ &
{\it abs}_c\ (R\ r)  \\
{\it rep} & : & \xi \rightarrow \tau  &
{\it rep}\ a  & \ \defeq \ &
\mbox{\tt \$@} \ ({\it rep}_c\ a)\ \ ( \ = \
\mbox{\tt @}r.\ {\it rep}_c\ a \ r
%\ = \ \mbox{\tt @}x.\ ( R\ x = {\it rep}_c\ a )
\ )
\end{array}
$$
\end{definition}

The {\tt @} operator
%which is here used as a prefix unary operator {\tt \$@},
is a higher order version of Hilbert's choice operator $\varepsilon$
\cite{GoMe93,Lei69}.
It has type $(\alpha \rightarrow \mbox{\tt bool}) \rightarrow \alpha$,
%{\tt ('a -> bool) -> 'a},
and is usually used as a binder,
where
%the two syntaxes are related by
$\mbox{\tt \$@}\ P = \mbox{\tt @}x.\ P\ x$.
(The {\tt \$} converts an operator to prefix syntax.)
%The axiom in HOL about the behavior of {\tt @} is
{\tt @} satisfies the HOL axiom
$\forall P\ x.\ P\ x \Rightarrow P\ (\mbox{\tt \$@}\ P)$.
Given any predicate $P$ on a type,
%(not confused with Definition \ref{quotient_type_def}),
if any element of the type satisfies the predicate,
then $\mbox{\tt \$@}\ P$ returns an arbitrary element of
that type which satisfies $P$.
If no element of the type satisfies $P$,
then $\mbox{\tt \$@}\ P$ will return simply some
arbitrary,
unknown
element of the type.
%
%In the definition above, {\tt @}
%selects some arbitrary representative $x$ such
%that the equivalence class of $x$ is the class representating $a$.
%
Such definitions
have been questioned by constructivist critics of the Axiom of Choice.
%are controversial.
An alternative design for quotients avoiding
%the Hilbert choice operator and
the Axiom of Choice
is described in section \ref{axiomofchoice}.

%\begin{lemma}
%\label{type_exists}
%$\exists c.\ P\ c$
%\end{lemma}
%Proof: Let $x$ be a value of type {\tt ty}.
%Then choose $c = \mbox{\it E\/}\ x$,
%and then $P\ c = P\ ( \mbox{\it E\/}\ x ) =
%     (\exists r : {\tt ty}.\ {\it E\/}\ x = \mbox{\it E\/}\ r)$.
%Then choose $r = x$.

\begin{lemma}
\label{ty_REL_SELECT_REL}
$\forall r.\
R\ r\ r \Rightarrow
(R\ (\mbox{\tt \$@} \ (R\ r)) = R\ r)$.
\end{lemma}
Proof:
The axiom for the {\tt @} operator is
$\forall P\ x.\ P\ x \Rightarrow P\ (\mbox{\tt \$@}\ P)$.
Taking $P = R\ r$ and $x = r$, we have
$R\ r\ r \Rightarrow R\ r\ (\mbox{\tt \$@}\ R\ r)$.
Assuming $R\ r\ r$,
$R\ r\ (\mbox{\tt \$@} \ (R\ r))$ follows.
%By lemma
%\ref{ty_REL_SELECT} and symmetry, $R\ (\mbox{\tt \$@} \ (R\ r))\ r$.
Then
by (\ref{PERinput}),
%since $R\ x\ y \Leftrightarrow R\ x\ x \wedge R\ y\ y \wedge (R\ x = R\ y)$
%(the partial equivalence property for $R$),
$R\ r\ (\mbox{\tt \$@} \ (R\ r))$ implies the equality
$R\ r = R\ (\mbox{\tt \$@} \ (R\ r))$.
$\Box$

\begin{theorem}
\label{ty_ABS_REP}
$\forall a.\ {\it abs}\ ({\it rep}\ a) = a$
\end{theorem}
Proof:
By Lemma \ref{ty_REP_REL}
 and the definition of $P$,
%By Corollary \ref{ty_REP_REL_cor},
for each $a$
there exists an $r$ such that
$R\ r\ r$ and ${\it rep}_c\ a = R\ r$.
Then
by Lemma \ref{ty_REL_SELECT_REL}, $R\ (\mbox{\tt \$@} \ (R\ r)) = R\ r$.
%which is equivalent to $R\ (\mbox{\tt \$@}\ ({\it rep}_c\ a) = {\it rep}_c\ a$.
Now by Definition \ref{abs_rep_def}, ${\it abs}\ ({\it rep}\ a) =
{\it abs}_c\ (R\ (\mbox{\tt \$@}\ ({\it rep}_c\ a)))$,
which simplifies by the above and Definition \ref{abs_rep_classes}(a)
to $a$. $\Box$
%equivalent to ${\it abs}_c\ ({\it rep}_c\ a)$,
%which by Definition \ref{abs_rep_classes} is simply $a$.
\begin{comment}
$$
\begin{array}{rcl@{\hspace{2.0cm}}r}
{\it abs}\ ({\it rep}\ a)
%\lceil \, \lfloor a \rfloor \, \rceil
& \ = \ &
{\it abs}_c\ (R\ (\mbox{\tt \$@}\ ({\it rep}_c\ a)))
%\lceil \, [ \, \mbox{\tt \$@} \ \lfloor a {\rfloor}_c \, ]_E {\rceil}_c
& \mbox{Definition \ref{abs_rep_def}}  \\
& \ = \ &
{\it abs}_c\ (R\ (\mbox{\tt \$@}\ (R\ r)))
%\lceil \, [ \, \mbox{\tt \$@} \ [ r ]_E \, ]_E {\rceil}_c
& \mbox{selection of $r$}  \\
& \ = \ &
{\it abs}_c\ (R\ r)
& \mbox{Lemma \ref{ty_REL_SELECT_REL} and $R\ r\ r$}  \\
& \ = \ &
{\it abs}_c\ ({\it rep}_c\ a)
\ = \ a
%& \mbox{selection of $r$}  \\
%& \ = \ &
%a
& \mbox{selection of $r$,} \
  \mbox{Definition \ref{abs_rep_classes}(a)}  \\
\Box \hfill & & &
\end{array}
$$
\end{comment}

\begin{theorem}
\label{rep_respects}
$\forall a.\ R\ ({\it rep}\ a)\ ({\it rep}\ a)$.
\end{theorem}
Proof:
As before,
%in Theorem \ref{ty_ABS_REP},
%By Lemma \ref{ty_REP_REL} and the definition of $P$,
%By Corollary \ref{ty_REP_REL_cor},
for each $a$
there exists an $r$ such that
$R\ r\ r$ and ${\it rep}_c\ a = R\ r$.
%Then
%by Definition \ref{abs_rep_def},
%$R\ ({\it rep}\ a)\ ({\it rep}\ a)$
%is $R\ (\mbox{\tt \$@}\ ({\it rep}_c\ a))\ (\mbox{\tt \$@}\ ({\it rep}_c\ a))$,
%which is $R\ (\mbox{\tt \$@}\ (R\ r))\ (\mbox{\tt \$@}\ (R\ r))$,
%which by Lemma \ref{ty_REL_SELECT_REL} twice,
%using the symmetry of $R$, is $R\ r\ r$, true.
%
$$
\begin{array}[t]{rcl@{\hspace{0.5cm}}r}
R\ (\mbox{\it rep}\ a)\ (\mbox{\it rep}\ a)
& \ \Leftrightarrow \ &
R\ (\mbox{\tt \$@}\ (\mbox{\it rep}_c\ a))\ (\mbox{\tt \$@}\ (\mbox{\it rep}_c\ a))
& \mbox{Definition \ref{abs_rep_def}}  \\
& \ \Leftrightarrow \ &
R\ (\mbox{\tt \$@}\ (R\ r))\ (\mbox{\tt \$@}\ (R\ r))
& \mbox{selection of $r$}  \\
& \ \Leftrightarrow \ &
R\ r\ (\mbox{\tt \$@}\ (R\ r))
& \mbox{Lemma \ref{ty_REL_SELECT_REL}}  \\
& \ \Leftrightarrow \ &
R\ (\mbox{\tt \$@}\ (R\ r))\ r
& \mbox{symmetry of $R$}  \\
& \ \Leftrightarrow \ &
R\ r\ r \ \Leftrightarrow \ T
& \mbox{Lemma \ref{ty_REL_SELECT_REL}, selection of $r$}  \\
\Box \hfill & & &
\end{array}
$$
%$\Box$

\begin{theorem}
\label{equiv_ty_ABS}
$\forall r\ s.\ \ R\ r\ s \ \Leftrightarrow \
R\ r\ r\ \wedge \ R\ s\ s\ \wedge \
({\it abs}\ r = {\it abs}\ s)$
\end{theorem}
Proof:
$
\begin{array}[t]{rcl@{\hspace{0.6cm}}r}
R\ r\ s
& \ \Leftrightarrow \ &
R\ r\ r \ \wedge\ R\ s\ s \ \wedge\ (R\ r = R\ s)
& \mbox{(\ref{PERinput})}  \\
& \ \Leftrightarrow \ &
R\ r\ r \ \wedge\ R\ s\ s \ \wedge\
({\it abs}_c\ (R\ r) = {\it abs}_c\ (R\ s))
& \mbox{Lemma \ref{ty_ABS_11}}  \\
%& \ \Leftrightarrow \ &
% \lceil E\ r {\rceil}_c = \lceil E\ s {\rceil}_c
%& \mbox{Definition \ref{equiv_class}}  \\
& \ \Leftrightarrow \ &
R\ r\ r \ \wedge\ R\ s\ s \ \wedge\
({\it abs}\ r = {\it abs}\ s)
& \mbox{Definition \ref{abs_rep_def}}  \\
\Box \hfill & & &
\end{array}
$

%Because $\lfloor \_ {\rfloor}_c$ is one-to-one,
%$\forall a\ a'.\ (\lfloor a {\rfloor}_c = \lfloor a' {\rfloor}_c) = (a = a')$,
%so the goal is equivalent to
%$$
%E\ r\ r' =
%  (\lfloor \, \lceil r \rceil \, {\rfloor}_c =
%   \lfloor \, \lceil r' \rceil \, {\rfloor}_c)
%$$
%By Definition \ref{abs_rep_def}, the goal is
%$$
%E\ r\ r' =
%  (\lfloor \, \lceil E\ r {\rceil}_c \, {\rfloor}_c =
%   \lfloor \, \lceil E\ r' {\rceil}_c \, {\rfloor}_c)
%$$
%By Theorem \ref{abs_rep_classes_simple}, this simplifies to
%$$
%E\ r\ r' =
%  (E\ r =
%   E\ r')
%$$
%which is proved by Lemma \ref{ty_REL_equiv}.

\begin{theorem}
\label{quotientthm}
$\langle R,\ {\it abs},\ {\it rep} \rangle$.
\end{theorem}
Proof:
By Theorems \ref{ty_ABS_REP},
\ref{rep_respects},
and
\ref{equiv_ty_ABS}, with Definition
\ref{quotientdef}.
$\Box$


%
\section{Aggregate and Higher Order Quotient Theorems}
%
\label{extensions}

Traditional quotients that lift $\tau$ to a set of $\tau$ also
lift lists of $\tau$ to sets of lists of $\tau$.
These sets are isomorphic to lists, but {\it they are not lists}.
In this design, when $\tau$ is lifted to $\xi$, then
we lift lists of $\tau$ to lists of $\xi$.
We preserve the type operator structure built on top of the
types being lifted.  Similarly, we want to preserve polymorphic constants.
Thus we need not create a new type for each lifted version of lists,
but simply reuse the existing list type operator, now applied to $\xi$.
This preserves the type structure and enables direct use
of the polymorphic constants of that type operator, such as
{\tt HD} for lists.
In a theorem being lifted, we want an occurrence of
$\mbox{\tt HD} : \tau\ \mbox{\tt list} \rightarrow \tau$
to lift to an occurrence of
$\mbox{\tt HD} : \xi\ \mbox{\tt list} \rightarrow \xi$.
%This motivated the design choice in
%This is vital.
If such a constant is not lifted to itself, the lifted version
of the theorem will not look like the original.
Hence Definition \ref{quotientdef} was
intentionally
designed
to preserve the vital type operator structure.
%so that $\tau$ could lift to any $\xi'$ isomorphic to $\xi$.

\begin{comment}
\end{comment}
At times one wishes to not only lift a number of types across a
quotient operation, but also lift by extension a number of other
types which are dependent on the first set.  For example, if we
lift the type of terms of the lambda calculus across alpha-equivalence,
then we would also expect that the types of lists or pairs involving
the lifted terms would follow naturally.

In fact these do follow; one merely has to apply the type
operator, say {\tt list}, to the lifted type {\tt term} to produce
the type of lists of lifted terms {\tt (term)list}.  All of the
theorems about lists in general now apply to lists of lifted terms,
and all of the theorems about lifted terms apply to the elements of
these lifted lists.
\begin{comment}
\end{comment}

%However, we will see that within the {\tt define\_quotient\_types} function,
In the process of lifting constants and theorems,
quotient theorems are needed for each
argument and result type
%subtype of the type
of each constant being lifted.
%where each type involved is a subtype of the type of the constant.
%either the type of a parameter or the type of the result.
For aggregate and higher order types,
the tool automatically proves any needed quotient theorems
%for the types
from the available quotient theorems for the
constituent subtypes.
To accomplish this, the tool uses {\it quotient extension theorems\/}
(section \ref{condquotients}).
These are provided preproven for some standard type operators.
For others,
%new types that the user may declare,
new quotient extension theorems may be manually proven and then
included to extend the tool's power.
%to handle the new types.
\begin{comment}
\end{comment}

%This section discusses the creation
%%and manipulation
%of these quotient
%theorems for aggregate types.

%
\subsection{Aggregate and Higher Order PERs and Map Operators}
%
\label{aggregates}

Some aggregate equivalence relation
operators have been already described in section \ref{equivalence}, and
these can equally be used to build aggregate \quotient{} relations.
In addition, for function types, the following is added:

\begin{center}
\framebox{
\begin{tabular}[t]{lrl}
Type & Operator \ \ \ \ \ & Type of operator \\
\hline \\
fun & {\tt ===> : } & {\tt ('a -> 'a -> bool) -> ('b -> 'b -> bool) ->} \\
& & {\tt \ \ \ \ \ \ ('a -> 'b) -> ('a -> 'b) -> bool}  \\
\end{tabular}
}
\end{center}

%\noindent
%The definition of the function relation operator is:
%
% related to respectfulness:
\begin{definition}
\label{funrel}
$(R_1\ \mbox {\tt ===>} \ R_2)\ f \ g \ \Leftrightarrow \
\forall x \ y. \ R_1\ x\ y \Rightarrow R_2\ (f\ x)\ (g\ y)$.
\end{definition}
%\begin{center}
%{\tt (R1 ===> R2) f g \Leftrightarrow
%   $\forall$x y. R1 x y $\Rightarrow$ R2 (f x) (g y)}.
%\end{center}

Note $R_1$ {\tt ===>} $R_2$ is {\it not\/} in general an equivalence relation
(it is not reflexive).
It is reflexive at a function $f$,
($R_1$ {\tt ===>} $R_2$) $f$ $f$,
if and only if $f$ is respectful.

% A quotient theorem relates a \quotient{} relation to abstraction
% and representation functions, which map between values of the original
% and quotient types.  These abstraction and representation functions
% for aggregate types
% can be formed by particular operators, again depending on the type operator
% involved, using the abstraction and representation functions of the
% constituent subtypes of the aggregate type.

%\begin{verbatim}
\begin{comment}
\end{comment}
To ease the creation of quotient theorems,
we provide several Standard ML functions that automatically prove the
necessary quotient theorems for lists, pairs, sums, options, and function types,
given the quotient theorems for the subtypes which are the arguments to
these type operators.

\begin{center}
\framebox{
\begin{tabular}[t]{rl}
{\tt list\_quotient} & {\tt : thm -> thm} \\
{\tt pair\_quotient} & {\tt : thm -> thm -> thm} \\
{\tt sum\_quotient} & {\tt : thm -> thm -> thm}  \\
{\tt option\_quotient} & {\tt : thm -> thm}  \\
{\tt fun\_quotient} & {\tt : thm -> thm -> thm}  \\
\\
{\tt identity\_quotient} & {\tt : hol\_type -> thm}  \\
{\tt make\_quotient} & {\tt : thm list -> hol\_type -> thm}  \\
\end{tabular}
}
\end{center}

These functions prove and return quotient theorems,
of the form
\begin{center}
$\vdash$ {\tt QUOTIENT} {\it R\/} {\it abs\/} {\it rep}
\end{center}
%created by
%as that returned by the function {\tt define\_quotient\_type}
%(see the bottom of page 4).
%
%These functions do not create new types, since the types are formed
%using the existing {\tt list}, {\tt prod}, {\tt sum}, {\tt option},
%and {\tt fun} type operators.
The first five functions all take as arguments quotient theorems
for the constituent subtypes that are arguments
to the aggregate type operator.  The last two take an {\tt hol\_type} as
an argument, which is the type of elements compared by the \quotient{} relation
of the desired quotient theorem.
None of these create any new types,
they simply apply existing type operators.

Sometimes one desires to perform the quotient operation on some
arguments of the type operator but not on others. In these
cases, to indicate an argument which is not to be changed,
supply in that place
a quotient theorem
%may be
created by the
{\tt identity\_quotient} function, which takes any HOL type and
returns the identity quotient theorem for that type,
using equality and the identity function,
%using simple equality ({\tt =}) and the identity function {\tt I},
%where the \quotient{} relation
%used in the quotient theorem is simple equality ({\tt =})
%between items of that type.

\begin{center}
{\tt $\vdash$ QUOTIENT (\$= : ty -> ty -> bool) (I: ty -> ty) (I: ty -> ty)}
\end{center}

In case one would need to create a quotient theorem for a complex type,
the {\tt make\_quotient} function takes a list of
%base (not aggregate)
quotient theorems and an HOL type, and returns a quotient theorem for
that type, automatically constructing it recursively
according to the structure of the type
and the supplied quotient theorems.
% for the bases.
\begin{comment}
\end{comment}
%\end{verbatim}

%(*      Type Operator     Constructor   Abstraction      Equivalence   *)
%(*                                                                     *)
%(*  Identity                  I x           I                $=        *)
%(*  Product  (ty1 # ty2)     (a,b)    (abs1 ## abs2)     (R1 ### R2)   *)
%(*  Sum      (ty1 + ty2)    (INL x)   (abs1 ++ abs2)     (R1 +++ R2)   *)
%(*  List      (ty list)    (CONS h t)    (MAP abs)       (LIST_REL R)  *)
%(*  Option    (ty option)  (SOME x)  (OPTION_MAP abs)   (OPTION_REL R) *)
%(*  Function (ty1 -> ty2)  (\x. f x)  (rep1 --> abs2)  (rep1 =-> abs2) *)
%(*  (Strong respect)                                     (R1 ===> R2)  *)

The quotient theorems
created for aggregate types
%returned by the aggregate quotient functions
involve not only aggregate \quotient{} relations, but also
aggregate abstraction and representation functions.  These are constructed
from the component abstraction and representation functions using the
following ``map'' operators.

\begin{center}
\framebox{
\begin{tabular}[t]{lrl}
Type & Operator \ \ \ \ \ & Type of operator, examples of {\it abs\/} and
{\it rep\/} fns \\
\hline \\
list & {\tt MAP : } & {\tt ('a -> 'b) -> 'a list -> 'b list} \\
& & \hspace{3mm} {\it examples:} ({\tt MAP} {\it abs}) , ({\tt MAP} {\it rep}) \\
\\
pair & {\tt \#\# : } & {\tt ('a -> 'b) -> ('c -> 'd) ->}  \\
& & {\tt \ \ \ \ 'a \# 'c -> 'b \# 'd} \\
& & \hspace{3mm} {\it examples:} (${\it abs}_1$ {\tt \#\#} ${\it abs}_2$) ,
	    (${\it rep}_1$ {\tt \#\#} ${\it rep}_2$)  \\
\\
sum & {\tt ++ : } & {\tt ('a -> 'b) -> ('c -> 'd) ->} \\
& & {\tt \ \ \ \ 'a + 'c -> 'b + 'd} \\
& & \hspace{3mm} {\it examples:} (${\it abs}_1$ {\tt ++} ${\it abs}_2$) ,
	    (${\it rep}_1$ {\tt ++} ${\it rep}_2$)  \\
\\
option\ \ & {\tt OPTION\_MAP : } & {\tt ('a -> 'b) -> 'a option -> 'b option} \\
& & \hspace{3mm} {\it examples:} ({\tt OPTION\_MAP} ${\it abs}$) ,
	    ({\tt OPTION\_MAP} ${\it rep}$)  \\
\\
fun & {\tt --> : } & {\tt ('a -> 'b) -> ('c -> 'd) ->} \\
& & {\tt \ \ \ \ ('b -> 'c) -> 'a -> 'd} \\
& & \hspace{3mm} {\it examples:} (${\it rep}_1$ {\tt -->} ${\it abs}_2$) ,
	    (${\it abs}_1$ {\tt -->} ${\it rep}_2$)  \\
% & & \hspace{3mm} {\it definition:}
% {\tt (f --> g) h x = g (h (f x))}  \\
\end{tabular}
}
\end{center}

\noindent
The definitions of the above operators are indicated below.
They are created either in the quotient package or in standard HOL.

\begin{definition}
\label{listmap}
$\begin{array}[t]{lccl}
\mbox{\tt MAP}\ f & \mbox{\tt []} & \ = \  & \mbox{\tt []} \\
\mbox{\tt MAP}\ f & (a \mbox{\tt ::} as) & \ = \
   & (f\ a)\ \mbox{\tt ::}\ (\mbox{\tt MAP}\ f\ as)
\end{array}$
\end{definition}

\begin{definition}
\label{pairmap}
$\begin{array}[t]{lccl}
(f_1\ \mbox{\tt \#\#}\ f_2) & (a_1, \ a_2) & \ = \
   & (f_1\ a_1, \ f_2\ a_2)
\end{array}$
\end{definition}

\begin{definition}
\label{summap}
$\begin{array}[t]{lccl}
(f_1\ \mbox{\tt ++}\ f_2) & (\mbox{\tt INL}\ a_1) & \ = \
   & \mbox{\tt INL}\ (f_1\ a_1)  \\
(f_1\ \mbox{\tt ++}\ f_2) & (\mbox{\tt INR}\ a_2) & \ = \
   & \mbox{\tt INR}\ (f_2\ a_2)
\end{array}$
\end{definition}

\begin{definition}
\label{optionmap}
$\begin{array}[t]{lccl}
\mbox{\tt OPTION\_MAP}\ f & \mbox{\tt NONE} & \ = \
   & \mbox{\tt NONE}  \\
\mbox{\tt OPTION\_MAP}\ f & (\mbox{\tt SOME}\ a) & \ = \
   & \mbox{\tt SOME}\ (f\ a)
\end{array}$
\end{definition}

The
%definition of the
function map operator definition is of special interest:

\begin{definition}
\label{funmap}
$(f\ \mbox{\tt -->}\ g)\ h\ x \ \defeq \
g\ (h\ (f\ x))$.
\end{definition}
%\begin{center}
%{\tt (f --> g) h x = g (h (f x))}.
%%{\tt f --> g = ($\lambda$h x. g (h (f x)))}.
%\end{center}

\noindent
{\tt MAP} and {\tt OPTION\_MAP} are prefix operators,
and the others are infix.
The identity quotient map operator is the identity operator
$\mbox{\tt I}:\alpha \rightarrow \alpha$.
%$\mbox{\tt I:'a} \rightarrow \mbox{\tt 'a}$.

These map operators are inserted automatically
in the quotient theorems created
for extended types.
%by the extended quotient functions.
Each resulting quotient theorem establishes that the extended type's
\quotient{} relation,
abstraction function, and representation function properly relate together
to form a quotient of the
%appropriate
extended type.

%The map operator definitions
%may be needed to prove
%the preservation
%%``definitions''
%of new polymorphic operators (see
%section \ref{polypreserves}).

%
\subsection{Quotient Extension Theorems}
%
\label{condquotients}

%%The
%%%{\tt define\_quotient\_types} and
%%{\tt make\_quotient}
%%function supports the extension of quotients
%%over any type operator for which a quotient extension theorem is
%%included in the first argument of {\tt make\_quotient}.
%%the list of theorems.
%A quotient extension theorem
%has antecedents
%%which are statements
%that the constituent subtypes
%of the type operator are quotients, and a consequent that states that the
%extension over the type operator is a quotient.
%Each antecedent has the form of a quotient theorem, but the types involved
%are simple type variables in the HOL logic.
%\begin{center}
%\begin{tabular}{rl}
%{\tt |-}
%& {\tt $\forall$R1 (abs1:$\alpha_1$->$\beta_1$) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ ...} \\
%%& {\tt ...} \\
%& {\tt $\forall$Rn (absn:$\alpha_n$->$\beta_n$) repn. QUOTIENT Rn absn repn $\Rightarrow$} \\
%& {\tt QUOTIENT (OP\_REL R1 ... Rn) (OP\_MAP abs1 ... absn rep1 ... repn)} \\
%&
%%\hspace{50mm}
%\hfill
%{\tt (OP\_MAP rep1 ... repn abs1 ... absn)}
%\end{tabular}
%\end{center}
%
%\noindent
%%where
%{\tt OP\_REL} creates a \quotient{} relation for the type operator
%$(\alpha_1,...,\alpha_n)op$.
%%as described in section \ref{equivalence}
%%or earlier in this section for the operator {\tt ===>} for function types,
%%and
%%where
%{\tt OP\_MAP} is a map operator which takes up to $2n$ arguments,
%%which are
%taken from
%%all
%%either
%the
%abstraction and representation functions
%between the types $\alpha_1$ through $\alpha_n$
%and $\beta_1$ through $\beta_n$.
%%respectively,
%%and,
%Depending on the order of the arguments, it
%yields either an abstraction or representation function
%between
%%the types
%$(\alpha_1,...,\alpha_n)op$
%and $(\beta_1,...,\beta_n)op$.

Here are the quotient extension theorems for the {\tt list}, {\tt prod},
{\tt sum}, {\tt option}, and, most significantly, {\tt fun} type operators:

{\tt \begin{tabbing}
LIS\=T\_QUOTIENT: \\
\>  $\vdash$ \=$\forall R\;$\=${\it abs}\;{\it rep}.\
          \langle R,{\it abs},{\it rep} \rangle \Rightarrow
          \langle \mbox{\tt LIST\_REL}\;R,\
            \mbox{\tt MAP}\;{\it abs},\ \mbox{\tt MAP}\;{\it rep} \rangle$ \\
%\>  $\vdash$ \=$\forall$R\= \ abs rep. QUOTIENT R abs rep $\Rightarrow$ \\
%\>\>\>   QUOTIENT (LIST\_REL R) (MAP abs) (MAP rep) \\
\\
PAIR\_QUOTIENT: \\
\>  $\vdash$   $\forall R_1\;{\it abs}_1\;{\it rep}_1.\
          \langle R_1,{\it abs}_1,{\it rep}_1 \rangle \Rightarrow \
          \forall R_2\;{\it abs}_2\;{\it rep}_2.\
          \langle R_2,{\it abs}_2,{\it rep}_2 \rangle \Rightarrow $ \\
\>\>\>   $\langle R_1\;\mbox{\tt \#\#\#}\;R_2,\
            {\it abs}_1\;\mbox{\tt \#\#}\;{\it abs}_2,\
            {\it rep}_1\;\mbox{\tt \#\#}\;{\it rep}_2
          \rangle$ \\
%\>  $\vdash$ $\forall$R1 abs1 rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\
%\>\>   $\forall$R2 abs2 rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\
%\>\>\>   QUOTIENT (R1 \#\#\# R2) (abs1 \#\# abs2) (rep1 \#\# rep2) \\
\\
SUM\_QUOTIENT: \\
\>  $\vdash$   $\forall R_1\;{\it abs}_1\;{\it rep}_1.\
          \langle R_1,{\it abs}_1,{\it rep}_1 \rangle \Rightarrow \
          \forall R_2\;{\it abs}_2\;{\it rep}_2.\
          \langle R_2,{\it abs}_2,{\it rep}_2 \rangle \Rightarrow $ \\
\>\>\>   $\langle R_1\;\mbox{\tt +++}\;R_2,\
            {\it abs}_1\;\mbox{\tt ++}\;{\it abs}_2,\
            {\it rep}_1\;\mbox{\tt ++}\;{\it rep}_2
          \rangle$ \\
%\>  $\vdash$ $\forall$R1 abs1 rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\
%\>\>   $\forall$R2 abs2 rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\
%\>\>\>   QUOTIENT (R1 +++ R2) (abs1 ++ abs2) (rep1 ++ rep2) \\
\\
OPTION\_QUOTIENT: \\
\>  $\vdash$   $\forall R\;{\it abs}\;{\it rep}.\
          \langle R,{\it abs},{\it rep} \rangle \Rightarrow $ \\
\>\>\>   $\langle \mbox{\tt OPTION\_REL}\;R,\
            \mbox{\tt OPTION\_MAP}\;{\it abs},\ \mbox{\tt OPTION\_MAP}\;{\it rep} \rangle$ \\
%\>  $\vdash$ $\forall$R abs rep. QUOTIENT R abs rep $\Rightarrow$ \\
%\>\>\>   QUOTIENT (OPTION\_REL R) (OPTION\_MAP abs) (OPTION\_MAP rep) \\
\\
FUN\_QUOTIENT: \\
\>  $\vdash$   $\forall R_1\;{\it abs}_1\;{\it rep}_1.\
          \langle R_1,{\it abs}_1,{\it rep}_1 \rangle \Rightarrow \
          \forall R_2\;{\it abs}_2\;{\it rep}_2.\
          \langle R_2,{\it abs}_2,{\it rep}_2 \rangle \Rightarrow $ \\
\>\>\>   $\langle R_1\;\mbox{\tt ===>}\;R_2,\
            {\it rep}_1\;\mbox{\tt -->}\;{\it abs}_2,\
            {\it abs}_1\;\mbox{\tt -->}\;{\it rep}_2
          \rangle$
%\>  $\vdash$ $\forall$R1 abs1 rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\
%\>\>   $\forall$R2 abs2 rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\
%\>\>\>   QUOTIENT (R1 ===> R2) (rep1 --> abs2) (abs1 --> rep2)
\end{tabbing}}

This last theorem is of central and critical importance to forming higher order
quotients.
We present here its proof in detail.

\begin{theorem}[Function quotients]
\label{funquotient}
If relations $R_1$ and $R_2$
with
%are \quotient{} relations with respect to
abstraction functions ${\it abs}_1$ and ${\it abs}_2$
and representation functions ${\it rep}_1$ and ${\it rep}_2$,
respectively,
are quotients,
then $R_1$ {\tt ===>} $R_2$
with
%is a \quotient{} relation with respect to
abstraction function ${\it rep}_1$ {\tt -->} ${\it abs}_2$
and representation function
${\it abs}_1$~{\tt -->}~${\it rep}_2$
is a quotient.

%If $R_1$ and $R_2$ are \quotient{}
%relations with respect to
%abstraction functions ${\it abs}_1$ and ${\it abs}_2$
%and representation functions ${\it rep}_1$ and ${\it rep}_2$,
%respectively,
%then $R_1$ {\tt ===>} $R_2$ is a \quotient{} relation with
%respect to
%abstraction function ${\it rep}_1$ {\tt -->} ${\it abs}_2$
%and representation function
%${\it abs}_1$~{\tt -->}~${\it rep}_2$.
\end{theorem}
{\bf Proof:}
We need to prove the three properties of
Definition \ref{quotientdef}:
%in section \ref{quotientrelation}:
% for $R_1$ {\tt ===>} $R_2$ to be a \quotient{} relation with
%respect to
% abstraction function ${\it rep}_1$ {\tt -->} ${\it abs}_2$
% and representation function ${\it abs}_1$ {\tt -->} ${\it rep}_2$:

{\it Property 1.} Prove for all $a$,
(${\it rep}_1$ {\tt -->} ${\it abs}_2$)
((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$) = $a$. \\
Proof:
The equality here is between functions, and by extension, true if
for all values $x$ in $a$'s domain,
(${\it rep}_1$ {\tt -->} ${\it abs}_2$)
((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$) $x$ = $a$ $x$. \\
By the definition of {\tt -->}, this is
${\it abs}_2$
((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$ (${\it rep}_1$ $x$)) = $a$ $x$,
and then
${\it abs}_2$ (${\it rep}_2$ ($a$ (${\it abs}_1$ (${\it rep}_1$ $x$)))) = $a$ $x$.
By Property 1 of $\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$,
${\it abs}_1$ (${\it rep}_1$ $x$) = $x$, and
by Property 1 of $\langle R_2$,${\it abs}_2$,${\it rep}_2 \rangle$,
$\forall b.\ {\it abs}_2$ (${\it rep}_2$ $b$) = $b$, so
this reduces to $a$ $x$ = $a$ $x$, true.

{\it Property 2.} Prove
($R_1$ {\tt ===>} $R_2$)
((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$)
((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$). \\
Proof:
By the definition of {\tt ===>}, this is \\
$\forall x, y.$
$R_1 \ x \ y \ \Rightarrow$ $R_2$
((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$ $x$)
((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$ $y$).
Assume $R_1 \ x \ y$, and show $R_2$
((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$ $x$)
((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$ $y$).
By the definition of {\tt -->}, this is $R_2$
(${\it rep}_2$ ($a$ (${\it abs}_1$ $x$)))
(${\it rep}_2$ ($a$ (${\it abs}_1$ $y$))).
Now since $R_1 \ x \ y$, by Property 3 of $\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$,
${\it abs}_1$ $x$ = ${\it abs}_1$ $y$.
Substituting this into our goal, we must prove $R_2$
(${\it rep}_2$ ($a$ (${\it abs}_1$ $y$)))
(${\it rep}_2$ ($a$ (${\it abs}_1$ $y$))).
But this is an instance of Property 2 of
$\langle R_2$,${\it abs}_2$,${\it rep}_2 \rangle$, and
so the goal is proven.

{\it Property 3.} Prove
($R_1$ {\tt ===>} $R_2$) $r$ $s$ $\Leftrightarrow$
%{\it (if and only if)}
\\
($R_1$ {\tt ===>} $R_2$) $r$ $r$ $\wedge$
($R_1$ {\tt ===>} $R_2$) $s$ $s$
%\hspace*{\fill}
$\wedge$
((${\it rep}_1$ {\tt -->} ${\it abs}_2$) $r$ =
(${\it rep}_1$ {\tt -->} ${\it abs}_2$) $s$). \\
The last conjunct on the right side is equality between functions, so by extension this is
($R_1$ {\tt ===>} $R_2$) $r$ $s$ $\Leftrightarrow$
($R_1$ {\tt ===>} $R_2$) $r$ $r$ $\wedge$
($R_1$ {\tt ===>} $R_2$) $s$ $s$ $\wedge$ \\
\hspace*{\fill}
($\forall x.$ (${\it rep}_1$ {\tt -->} ${\it abs}_2$) $r$ $x$ =
	 (${\it rep}_1$ {\tt -->} ${\it abs}_2$) $s$ $x$). \\
By the definitions of {\tt ===>} and {\tt -->}, this is
$(1) \Leftrightarrow (2) \wedge (3) \wedge (4)$, where
\begin{center}
\begin{tabular}{r@{\hspace{10mm}}l}
(1) &
($\forall x\ y.\ R_1 \ x \ y \ \Rightarrow$ $R_2$ ($r$ $x$) ($s$ $y$))
 \\
(2) &
($\forall x\ y.\ R_1 \ x \ y \ \Rightarrow$ $R_2$ ($r$ $x$) ($r$ $y$))
\\
(3) &
($\forall x\ y.\ R_1 \ x \ y \ \Rightarrow$ $R_2$ ($s$ $x$) ($s$ $y$))
\\
(4) &
($\forall x.$ (${\it abs}_2$ ($r$ (${\it rep}_1$ $x$)) =
	  ${\it abs}_2$ ($s$ (${\it rep}_1$ $x$))).  \\
\end{tabular}
\end{center}
We prove
$(1) \Leftrightarrow (2) \wedge (3) \wedge (4)$
as a biconditional with two goals.
%
%\begin{center}
%\begin{tabular}{r@{\hspace{10mm}}l}
%(1) &
%($\forall x,y.\ R_1 \ x \ y \ \Rightarrow$ $R_2$ ($r$ $x$) ($s$ $y$))
%=  \\
%(2) &
%\hspace{3mm}
%($\forall x,y.\ R_1 \ x \ y \ \Rightarrow$ $R_2$ ($r$ $x$) ($r$ $y$))
%$\wedge$ \\
%(3) &
%\hspace{3mm}
%($\forall x,y.\ R_1 \ x \ y \ \Rightarrow$ $R_2$ ($s$ $x$) ($s$ $y$))
%$\wedge$ \\
%(4) &
%\hspace{3mm}
%($\forall x.$ (${\it abs}_2$ ($r$ (${\it rep}_1$ $x$)) =
%	  ${\it abs}_2$ ($s$ (${\it rep}_1$ $x$))).  \\
%\end{tabular}
%\end{center}
% (1)   ($\forall$x y. R1 x y $\Rightarrow$ R2 (r x) (s y)) =
% (2)   ($\forall$x y. R1 x y $\Rightarrow$ R2 (r x) (r y)) /\
% (3)   ($\forall$x y. R1 x y $\Rightarrow$ R2 (s x) (s y)) /\
% (4)   $\forall$x. abs2 (r (rep1 x)) = abs2 (s (rep1 x))
%The equality at the end of the first line is between booleans.
%We prove this as a biconditional with two goals.

{\it Goal 1.}
($\Rightarrow$)
Assume (1).  Then we must prove (2), (3), and (4).

{\it Subgoal 1.1.} (Proof of (2))
Assume $R_1$ $x$ $y$.  We must prove $R_2$ ($r$ $x$) ($r$ $y$).
From $R_1$ $x$ $y$ and Property 3 of
$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$,
we also have
$R_1$ $x$ $x$ and
$R_1$ $y$ $y$.
From (1) and $R_1$ $x$ $y$, we have $R_2$ ($r$ $x$) ($s$ $y$).
From (1) and $R_1$ $y$ $y$, we have $R_2$ ($r$ $y$) ($s$ $y$).
Then by symmetry and transitivity of $R_2$, the goal is proven.

{\it Subgoal 1.2.} (Proof of (3)) Similar to the previous subgoal.

{\it Subgoal 1.3.} (Proof of (4))
%Show
%   ${\it abs}_2$ ($r$ (${\it rep}_1$ $x$)) =
%   ${\it abs}_2$ ($s$ (${\it rep}_1$ $x$)).
$R_1$ (${\it rep}_1$ $x$) (${\it rep}_1$ $x$) follows from
Property 2 of
$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$.
From (1),
we have
$R_2$ ($r$ (${\it rep}_1$ $x$)) ($s$ (${\it rep}_1$ $x$)).
Then the goal follows from this and the third conjunct of Property 3 of
$\langle R_2$,${\it abs}_2$,${\it rep}_2 \rangle$.

{\it Goal 2.} ($\Leftarrow$)
Assume (2), (3), and (4).  We must prove (1).
Assume $R_1\ x\ y$.  Then we must prove $R_2$ ($r$ $x$) ($s$ $y$).
From $R_1\,x\ y$ and Property 3 of
$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$,
we also have
$R_1\,x\ x$,
$R_1\,y\ y$, and
${\it abs}_1$ $x$ = ${\it abs}_1$ $y$.
By Property 3 of
$\langle R_2$,${\it abs}_2$,${\it rep}_2 \rangle$,
the goal is
$R_2$ ($r$ $x$) ($r$ $x$) $\wedge$
$R_2$ ($s$ $y$) ($s$ $y$) $\wedge$
${\it abs}_2$ ($r$ $x$) = ${\it abs}_2$ ($s$ $y$).
This breaks into three subgoals.

{\it Subgoal 2.1.} Prove $R_2$ ($r$ $x$) ($r$ $x$).
This follows from
$R_1$ $x$ $x$ and (2).

{\it Subgoal 2.2.} Prove $R_2$ ($s$ $y$) ($s$ $y$).
This follows from
$R_1$ $y$ $y$ and (3).

\pagebreak[3]
{\it Subgoal 2.3.} Prove ${\it abs}_2$ ($r$ $x$) = ${\it abs}_2$ ($s$ $y$).
%\begin{lemma}
\begin{center}
\begin{minipage}{3.8in}
%\addtolength{\leftmargin}{1.0cm}
{\bf Lemma.} {\it
If
$\langle R$,${\it abs}$,${\it rep} \rangle$
and
$R$ $z$ $z$, then {\rm $R$ (${\it rep}$ (${\it abs}$ $z$)) $z$}.
%\end{lemma}
} \\
$R$ (${\it rep}$ (${\it abs}$ $z$)) (${\it rep}$ (${\it abs}$ $z$)),
by Property 2 of
$\langle R$,${\it abs}$,${\it rep} \rangle$.
%We already have
From the hypothesis,
$R$ $z$ $z$.
From Property 1 of
$\langle R$,${\it abs}$,${\it rep} \rangle$,
\linebreak[3]
${\it abs}$~(${\it rep}$ (${\it abs}$ $z$)) = ${\it abs}$ $z$.
From these three statements and Property 3 of
$\langle R$,${\it abs}$,${\it rep} \rangle$,
we have
$R$~(${\it rep}$ (${\it abs}$ $z$)) $z$.
%If
%$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$
%and
%$R_1$ $z$ $z$, then {\rm $R_1$ (${\it rep}_1$ (${\it abs}_1$ $z$)) $z$}.
%%\end{lemma}
%} \\
%$R_1$ (${\it rep}_1$ (${\it abs}_1$ $z$)) (${\it rep}_1$ (${\it abs}_1$ $z$)),
%by Property 2 of
%$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$.
%%We already have
%From the hypothesis,
%$R_1$ $z$ $z$.
%From Property 1 of
%$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$,
%\linebreak[3]
%${\it abs}_1$~(${\it rep}_1$ (${\it abs}_1$ $z$)) = ${\it abs}_1$ $z$.
%From these three statements and Property 3 of
%$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$,
%we have
%$R_1$~(${\it rep}_1$ (${\it abs}_1$ $z$)) $z$.
%
$\Box$
\end{minipage}
\end{center}
%\addtolength{\leftmargin}{-1.0cm}

By the lemma and $R_1$ $x$ $x$, we have
$R_1$~(${\it rep}_1$ (${\it abs}_1$ $x$)) $x$.
Similarly,
by the lemma and $R_1$ $y$ $y$, we have
$R_1$~(${\it rep}_1$ (${\it abs}_1$ $y$)) $y$.
Then by (2), we have
\linebreak[3]
$R_2$~($r$ (${\it rep}_1$ (${\it abs}_1$ $x$))) ($r$ $x$), and
by (3),
$R_2$~($s$~(${\it rep}_1$ (${\it abs}_1$ $y$))) ($s$ $y$).
From these and Property 3 of
$\langle R_2$,${\it abs}_2$,${\it rep}_2 \rangle$,
\begin{center}
\begin{tabular}{rcl}
${\it abs}_2$ ($r$ (${\it rep}_1$ (${\it abs}_1$ $x$)))
& = & ${\it abs}_2$ ($r$ $x$)
and \\
${\it abs}_2$ ($s$ (${\it rep}_1$ (${\it abs}_1$ $y$)))
& = & ${\it abs}_2$ ($s$ $y$).
\end{tabular}
\end{center}
But by ${\it abs}_1$ $x$ = ${\it abs}_1$ $y$ and (4),
the left hand sides of these two equations are equal, so
their right hand sides must be also,
${\it abs}_2$ ($r$ $x$) = ${\it abs}_2$ ($s$ $y$), which proves the goal.
$\Box$


%
\section{The Axiom of Choice}
%
\label{axiomofchoice}

Gregory Moore wrote that ``Rarely have the practitioners of mathematics,
a discipline known for the certainty of its conclusions, differed so vehemently
over one of its central premises as they have done over the Axiom of Choice.
Yet without the Axiom, mathematics today would be quite different''
\cite{Moore82}.
Today,
%a hundred years after Zermelo formulated the Axiom of Choice in 1904,
this discussion continues.
%in particular within the field of mechanical theorem proving.
Some theorem provers are based on classical logic,
and others on
%while others choose
%the restrictions of
a constructivist logic.
In higher order logic, the Axiom of Choice is represented
by Hilbert's $\varepsilon$-operator \cite[\S4.4]{Lei69},
also called the indefinite description
operator.
%\cite[\S 5.10]{NiPaWe02}.
  Paulson's lucid recent work \cite{LP04} exhibits an approach to quotients
which avoids the use of Hilbert's $\varepsilon$-operator,
by
instead
using the definite description operator~$\iota$
\cite[\S 5.10]{NiPaWe02}.
%\cite[ch.IV \S 4.1]{Lei69}
These two operators may be axiomatized as follows:
%\begin{eqnarray*}
%& \forall P\ x.\ P\ x \Rightarrow P (\varepsilon \ P) &
%\\
%& \forall P\ x.\ P\ x \Rightarrow (\forall y.\ P\ y \Rightarrow x = y) \Rightarrow P (\iota \ P) &
%\end{eqnarray*}
%or equivalently, in a manner which shows their similarity,
%\begin{eqnarray*}
%& \forall P.\ (\exists x.\ P\ x) \Rightarrow P (\varepsilon \ P) &
%\\
%& \forall P.\ (\exists ! x.\ P\ x) \Rightarrow P (\iota \ P) &
%\end{eqnarray*}
%
$$\begin{array}{cp{3mm}cp{3mm}c}
\forall P\ x.\ P\ x \Rightarrow P (\varepsilon \ P) & & or & &
\forall P.\ (\exists x.\ P\ x) \Rightarrow P (\varepsilon \ P)
\\
\forall P\ x.\ P\ x \Rightarrow (\forall y.\ P\ y \Rightarrow x = y) \Rightarrow P (\iota \ P) & & or & &
\forall P.\ (\exists ! x.\ P\ x) \Rightarrow P (\iota \ P)
\end{array}
$$

\noindent
The $\iota$-operator yields the single element of a singleton set,
$\iota \{z\} = z$, but its result on non-singleton sets is indeterminate.
By contrast, the $\varepsilon$-operator chooses some
indeterminate
element of any non-empty set, even if nondenumerable.
%where the particular element chosen is indeterminate.
%
%The $\varepsilon$-operator is weaker than the Axiom of Choice, as
%Leisenring states that ``it does not necessarily follow that the axiom
%of choice is derivable in a formulization of set theory
%which is based on the $\varepsilon$-calculus'' \cite{Lei69}.
%Nevertheless,
The $\iota$-operator is
%strictly
weaker than the $\varepsilon$-operator,
and less objectionable to constructivists.
%The Hilbert $\varepsilon$-operator
%expresses the description of an object whose existence
%is known without giving a method for constructing it or identifying
%exactly which object is chosen, which
%are key features of the Axiom of Choice.

Thus it is of interest to determine if a design for higher order quotients
may be formulated using only $\iota$, not $\varepsilon$.
Inspired by
%Paulson's work,
%Following
Paulson,
we
investigate this
by forming an alternative design,
eliminating the representation functions.
%redefine quotients.
%Inspired by Paulson's work,
%we can redefine
% the definition of
%quotients as follows.

\begin{definition}[Constructive quotient, replacing Definition \ref{quotientdef}]
\label{quotientdef_ac}
%We define that
\\
A relation {\it R\/}
with
%is a {\it \quotient{} relation\/} with respect to
abstraction function {\it abs\/}
% and representation function {\it rep\/}
(between the representation type $\tau$ and the abstraction type $\xi$)
is a {\it quotient}
% (notated as $\langle R$,${\it abs}$,${\it rep} \rangle$)
(notated as $\langle R, {\it abs} \rangle$)
if and only if
%the following hold:
\end{definition}

\begin{center}
\begin{tabular}[t]{l@{\hspace{0.5cm}}l}
%{\it existence of rep}
(1)
& $\forall a:\xi.\ \exists r:\tau.$
{\it R\/} $r$ $r$ $\wedge$ ({\it abs\/} $r$ = $a$) \\
%{\it partial equivalence}
(2)
& $\forall r\ s:\tau.$
{\it R\/} $r$ $s$ $\Leftrightarrow$
{\it R\/} $r$ $r$ $\wedge$
{\it R\/} $s$ $s$ $\wedge$
({\it abs} $r$ = {\it abs} $s$) \\
\end{tabular}
\end{center}

Property 1 states that for every abstract element $a$ of $\xi$
there exists a representative in $\tau$ which respects {\it R\/} and whose abstraction is $a$.
%and lifts to $a$.

Property 2 states that two elements of $\tau$ are related by {\it R\/}
if and only if
each element respects {\it R\/} and their abstractions are equal.

The quotients for new quotient types
based on (partial) equivalence relations may now be
constructed by a modified version of \S \ref{quotienttypes},
where the representation function {\it rep\/} is omitted
from Definition \ref{abs_rep_def}, so there is no
use of the Hilbert $\varepsilon$-operator.
Property 1 follows from Lemma \ref{ty_REP_REL}.
%and Property 2
%follows from Theorem
%\ref{equiv_ty_ABS}, as before.
%
The identity quotient is
$\langle \mbox{\tt \$=},\mbox{\tt I} \rangle$.
From Definition \ref{quotientdef_ac}
also follow analogs of the quotient extension theorems, e.g.,
$$
\forall R\ \mbox{\it abs}.\ \,
\langle R,\ \mbox{\it abs} \rangle \Rightarrow
\langle \mbox{\tt LIST\_REL}\ R,\ \mbox{\tt MAP}\ \mbox{\it abs} \rangle$$
\noindent
for lists
and similarly for pairs, sums and option types.
Functions are lifted by
the abstraction operation for functions, which requires two new definitions:
\begin{eqnarray*}
(abs \repofabs R) \ a \ r \ & \defeq & \
R\ r\ r\ \wedge \ {\it abs}\ r = a
\\
(reps \ \mbox{\tt +->} \ abs) \ f \ x \ & \defeq & \
\iota \ ({\tt IMAGE}\ {\it abs}\ ({\tt IMAGE}\ f\ ({\it reps}\ x)))
\end{eqnarray*}
%
\begin{comment}
\begin{eqnarray*}
abs \repofabs R \ & \defeq & \
\lambda a{\mbox{\tt :}\xi}.\
\lambda r{\mbox{\tt :}\tau}.\
R\ r\ r\ \wedge \ {\it abs}\ r = a
\\
rep \ \mbox{\tt +->} \ abs \ & \defeq & \
\lambda f
%:\alpha \rightarrow \beta
.\ \lambda x.\
\iota \ ({\tt IMAGE}\ {\it abs}\ ({\tt IMAGE}\ f\ ({\it rep}\ x)))
\end{eqnarray*}
\end{comment}

\noindent
%Constants are lifted using this abstraction operator {\tt +->}.
Note that for the identity quotient, $(\mbox{\tt I $\repofabs$ \$=}) = \mbox{\tt \$=}$.

The critical quotient extension
theorem for functions has also been proven:
\begin{theorem}[Function quotient extension]
\label{functionquotient}
$$
%\forall R_1\ {\it abs}_1\ R_2\ {\it abs}_2.\
  \langle R_1,\ {\it abs}_1 \rangle \Rightarrow
  \langle R_2,\ {\it abs}_2 \rangle \Rightarrow
\langle R_1 \ \mbox{\tt ===>} \ R_2,\
  ({\it abs}_1 \repofabs R_1) \ \mbox{\tt +->} \ {\it abs}_2 \rangle$$
\end{theorem}
\noindent
Unfortunately, the proof requires using the Axiom of Choice.
In fact, this theorem implies the Axiom of Choice, in that it implies
the existence of an operator which obeys the axiom of the
Hilbert $\varepsilon$-operator, as seen by the following development.

\begin{theorem}[Partial abstraction quotients]
\label{partabsquotient}
%If $f{\tt :} \alpha \rightarrow \beta$ is any function,
If $f$ is any function from type $\alpha$ to $\beta$,
and
%$Q{\tt :} \alpha \rightarrow {\tt bool}$ is any predicate,
$Q$ is any predicate on $\alpha$,
such that $\forall y{\tt :}\beta.\ \exists x{\tt :}\alpha.\ Q\ x \wedge (f\;x = y)$,
then the partial equivalence relation $R = \lambda r\;s.\ Q\ r \wedge Q\ s \wedge (f\;r = f\;s)$
with abstraction function $f$ is a quotient ($\langle R,f \rangle$).
\end{theorem}
{\bf Proof:}
%The two properties of Definition \ref{quotientdef_ac}
Follows easily from substituting $R$
in Definition \ref{quotientdef_ac}
%as defined above
and simplifying.
$\Box$

\begin{theorem}[Partial inverses exist]
\label{partinverses}
If $f$ is any function from type $\alpha$ to $\beta$, and $Q$ is any
predicate on $\alpha$,
such that $\forall y{\tt :}\beta.\ \exists x{\tt :}\alpha.\ Q\ x \wedge (f\ x = y)$,
then there exists a function $g$ such that
%$(\mbox{\tt \$=}\ \mbox{\tt ===>}\ R)\ g\ g \wedge
$f \circ g = {\tt I}$
% \wedge
and
%$(\forall x.\ Q\ (g\ x))$.
$\forall y.\ Q\ (g\ y)$.
{\rm
%Due in part to Dr.
[William Schneeburger]}
\end{theorem}
{\bf Proof:}
Assuming the function quotient extension theorem
%(Th.
\ref{functionquotient},
we apply it to two quotient theorems;
first, the identity quotient
$\langle \mbox{\tt \$=}, \mbox{\tt I} \rangle$
for type $\beta$, and second,
the partial abstraction quotient $\langle R,f \rangle$
from Theorem \ref{partabsquotient}.
This yields the quotient
$\langle \mbox{\tt \$=}\ \mbox{\tt ===>}\ R,\
% (\mbox{\tt I $\repofabs$ \$=})
 \mbox{\tt \$=}\ \mbox{\tt +->}\ f \rangle$,
since $(\mbox{\tt I $\repofabs$ \$=}) = \mbox{\tt \$=}$.
By Property 1 of Definition \ref{quotientdef_ac},
$\forall a.\ \exists r.\ (\mbox{\tt \$=}\ \mbox{\tt ===>}\ R)\ r\ r \wedge
((
\mbox{\tt \$=}
\ \mbox{\tt +->}\ f) r = a)$.
Specializing $a = {\tt I}:\beta \rightarrow \beta$,
and renaming $r$ as $g$, we obtain
$\exists g.\ (\mbox{\tt \$=}\ \mbox{\tt ===>}\ R)\:g\ g \wedge
(\mbox{\tt \$=}\ \mbox{\tt +->}\ f) g = {\tt I})$.
By the definition of $\mbox{\tt ===>}$,
$(\mbox{\tt \$=}\ \mbox{\tt ===>}\ R)\:g\ g$ is
$\forall x\ y.\ x = y \Rightarrow R\ (g\ x)\ (g\ y)$,
which simplifies by the definition of {\it R\/} to $\forall y.\ Q\ (g\ y)$.
The right conjunct is
$
%\exists g.\
(\mbox{\tt \$=}\ \mbox{\tt +->}\ f) g = {\tt I}$,
which by the definition of {\tt +->} is
%which is
$
%\exists g.
(\lambda x.\
\iota \ ({\tt IMAGE}\ {\it f}\ ({\tt IMAGE}\ g\ (\mbox{\tt \$=}\ x))))
 = {\tt I}$.
But $\mbox{\tt \$=}\ x$ is the singleton $\{x\}$,
so since ${\tt IMAGE}\ {\it h}\ \{z\} = \{h\ z\}$,
$\iota \{z\} = z$,
and $(\lambda x.\ f\ (g\ x)) = f \circ g$,
this
%is equivalent
simplifies
to $
%\exists g.
%(\lambda x.\ f\ (g\ x)) = {\tt I}$,
f \circ g = {\tt I}$,
and
the conclusion follows.
$\Box$

\begin{theorem}[Existence of Hilbert choice]
\label{hilbertchoice}
There exists an operator $c:(\alpha \rightarrow {\tt bool}) \rightarrow \alpha$
which obeys the Hilbert choice axiom,
$\forall P\ x.\ P\ x \Rightarrow P\ (c\ P)$.
\end{theorem}

{\bf Proof:}
In Theorem \ref{partinverses},
let $Q = (\lambda(P{\tt :}\alpha \rightarrow {\tt bool},\ a{\tt :}\alpha).\
                  (\exists x.\ P\ x) \Rightarrow P\ a)$
and $f = {\tt FST}$.  Then its antecedent is
$\forall P'.\, \exists (P,a).\, ((\exists x. P\, x) \Rightarrow P\, a) \wedge ({\tt FST} (P,a) = P')$.
For any $P'$,
take $P = P'$, and
if $\exists x.\ P\ x$,
then take $a$ to be such an $x$.
Otherwise take $a$ to be any value of $\alpha$.
In either case the antecedent is true.
%So
Therefore
by Theorem \ref{partinverses}
there exists a function $g$ such that
${\tt FST} \circ g = {\tt I}$
and
$\forall P.\ Q\ (g\ P)$,
which is
%$\forall P.\ {\bf let}\ (P,a) = g\ P\ {\bf in}\
$\forall P.\
(\exists x.\ ({\tt FST}\ (g\ P))\ x) \Rightarrow ({\tt FST}\ (g\ P))\ ({\tt SND}\ (g\ P))$.
The operator $c$ is
taken as ${\tt SND} \circ g$,
and
since ${\tt FST}\ (g\ P) = P$,
the Hilbert choice axiom follows.
$\Box$

\begin{comment}
{\bf Proof:}
In Theorem \ref{partinverses},
take $Q = (\lambda(P{\tt :}\alpha \rightarrow {\tt bool},\ a{\tt :}\alpha).\
                  (\exists x.\ P\ x) \Rightarrow P\ a)$
and $f = {\tt FST}$.  Then its antecedent is
$\forall P.\ \exists (P,a).\ ((\exists x.\ P\ x) \Rightarrow P\ a) \wedge ({\tt FST} (P,a) = P)$.
For any $P$, if $\exists x.\ P\ x$,
then take $a$ to be such an $x$.
Otherwise take $a$ to be any value of $\alpha$.
In either case the antecedent is true.
%So
Therefore there exists a function $g$ such that
${\tt FST} \circ g = {\tt I}$
and
$\forall P.\ {\bf let}\ (P,a) = g\ P\ {\bf in}\ ((\exists x.\ P\ x) \Rightarrow P\ a)$.
The operator $c$ is then taken as ${\tt SND} \circ g$,
and the Hilbert choice axiom follows.
$\Box$
\end{comment}

\vspace{2.0mm}
The significance of Theorem \ref{hilbertchoice}
is that even if we are able to avoid all use of the Axiom of Choice up to
this point, it is not possible to prove the function quotient extension
theorem \ref{functionquotient} without it.
This section's design may be used
to build a theory of quotients which is constructive and which extends
naturally to quotients of lists, pairs, sums, and options.
However, it is not possible
to extend it to higher order quotients while remaining constructive.
Therefore
the designs presented in this paper cannot be used to create higher order
quotients in strictly constructive theorem provers.
Alternatively, in theorem
provers like HOL which admit the Hilbert choice operator,
%there is no point
%in avoiding its use if we wish to enjoy higher order quotients
%although an automatic system for lifting theorems could be constructed,
%analogous to that for the main design,
if higher order quotients are desired,
there is no advantage in avoiding using the Axiom of Choice
through using the design of this section.
%as long as
The main design presented earlier is much simpler to automate.


\vfill
\pagebreak[4]
%
\section{Lifting Types, Constants, and Theorems}
%
\label{liftingall}

The definition of new types corresponding to the quotients of
existing types by equivalence relations is called ``lifting''
the types from a lower, more representational level to a higher,
more abstract level.  Both levels describe similar objects, but
some details which are apparent at the lower level are no longer
visible at the higher level.  The logic is simplified.

However, simply forming a new type does not complete the quotient operation.
Rather, one wishes to recreate the
%significant parts of the
pre-existing logical environment at the new,
higher, and more abstract level.  This includes not only the new
types, but also new versions of the constants that form and
manipulate values of those types, and also new versions of the
theorems that describe properties of those constants.  All of these
%must be recreated at the higher level, in order to
form a logical layer, above which all the lower representational details
may be safely and forever forgotten.

%Essentially what we wish to do is to consider the entire environment
%of tools and capabilities to prove theorems that existed at the lower
%level, and recreate those capabilities at the higher level.  This has
%three basic steps:
%
%\begin{enumerate}
%\item Lift the types,
%\item Lift the definitions of constants (including functions) on those types,
%\item Lift the theorems about the properties of those constants.
%\end{enumerate}

This can be done in a single call of the
main tool of this package.
%This one call
%defines the new types, lifts the definitions of constants,
%and proves at the higher level the lifted versions of theorems.

\begin{verbatim}
define_quotient_types :
        {types: {name: string,
                 equiv: thm} list,
         defs: {def_name: string,
                fname: string,
                func: Term.term,
                fixity: Parse.fixity} list,
         tyop_equivs : thm list,
         tyop_quotients : thm list,
         tyop_simps : thm list,
         respects : thm list,
         poly_preserves : thm list,
         poly_respects : thm list,
         old_thms : thm list} ->
        thm list
\end{verbatim}

{\tt define\_quotient\_types} takes a single argument which is a
record with the following fields.

{\it types\/} is a list of records, each of which contains two fields:
{\it name}, which is the name of a new quotient type to be created, and
{\it equiv}, which is
either 1)
a theorem that a binary relation {\it R\/}
is an equivalence relation
(see section \ref{equivalence}),
or 2)\ a theorem that {\it R\/} is a nonempty partial equivalence relation,
of the form
$$
\vdash\
(\exists x.\ R\ x\ x) \ \wedge \
(\forall x\ y.\ R\ x\ y \ \Leftrightarrow \
                R\ x\ x \wedge R\ y\ y \wedge (R\ x = R\ y))
$$
%,
%of the form:
%
%\begin{center}
%{\tt $\vdash\ \forall$x y. {\it R} x y = ({\it R} x = {\it R} y)}
%\end{center}
\noindent
or using the abbreviated forms
$\vdash \mbox{\tt EQUIV}\ R$
or
$\vdash \mbox{\tt PARTIAL\_EQUIV}\ R$, respectively.

{\it defs\/} is a list of records specifying the constants to be lifted.
Each record contains the following four fields:
{\it func\/} is an HOL term, which must be a single constant, which is the
constant to be lifted.
{\it fname\/} is the name of the new constant being defined as the lifted version of {\it func}.
{\it fixity\/} is the HOL fixity of the new constant being created,
as specified in the HOL structure {\tt Parse}.
{\it def\_name} is the name under which the new constant definition is to
be stored in the current theory.
%These fields, and the
The
process of defining lifted constants
%This
is described in
\S\ref{liftingdefs}.
%section \ref{liftingdefs}.

{\it tyop\_equivs\/} is a list of equivalence extension theorems
for type operators
(see
%section
\S\ref{condequivs}).  These are used for
bringing into regular form
theorems on new type operators, so that they can be lifted
(see sections \ref{restrictions} and
\ref{nonstandard}).

{\it tyop\_quotients\/} is a list of quotient extension theorems
for type operators
(see
%section
\S\ref{condquotients}).  These are used for lifting both constants
and theorems.

{\it tyop\_simps\/} is a list of theorems used to simplify type operator
relations and map functions for identity quotients, e.g.,
for pairs,
$\vdash (\mbox{\tt \$= \#\#\# \$=}) = \mbox{\tt \$=}$ and
$\vdash (\mbox{\tt I \#\# I}) = \mbox{\tt I}$,
or for lists,
$\vdash \mbox{\tt LIST\_REL \$=} = \mbox{\tt \$=}$ and
$\vdash \mbox{\tt MAP I} = \mbox{\tt I}$.

The rest of the arguments refer to the general process of lifting theorems
over the quotients being defined,
as described in section \ref{liftingtheorems}.

{\it respects\/} is a list of theorems about the respectfulness of the
constants being lifted.
These theorems are described in section
\ref{respectfulness}.

{\it poly\_preserves\/} is a list of theorems about the preservation of
polymorphic constants in the HOL logic
across a quotient operation.
%as if they were definitions across the quotient operation.
In other words, they state that any quotient operation preserves these
constants as a homomorphism.
These theorems are described in section
\ref{polypreserves}.

{\it poly\_respects\/} is a list of theorems showing the respectfulness
of the polymorphic constants mentioned in {\it poly\_preserves}.
These are
described in
\S
%section
\ref{polyrespects}.

{\it old\_thms\/} is a list of theorems concerning the lower, representative
types and contants, which are to be automatically lifted and proved at the
higher, more abstract quotient level.
These theorems are described in section \ref{oldtheorem}.

{\tt define\_quotient\_types} returns a list of theorems, which are the
lifted versions of the {\it old\_thms}.

A similar function,
{\tt define\_quotient\_types\_rule}, takes a single argument which is a
record with the same fields as above except for {\it old\_thms},
and returns an SML function of type {\tt thm -> thm}.
This result, typically called {\tt LIFT\_RULE},
is then used to lift the old theorems individually, one at a time.

In addition to these, two related functions,
{\tt define\_quotient\_full\_types} and
{\tt define\_quotient\_full\_types\_rule},
are provided
that automatically include the standard pre-proven quotient,
equivalence, and simplification theorems relating
to the list, pair, sum, option, and function type operators, along with
all the pre-proven polymorphic respectfulness and preservation theorems
for many standard polymorphic operators of those theories in HOL.
Other type operators and/or polymorphic operators may be supported
by including their theorems in the appropriate input fields, which
are named the same as before.

%This function is limited to a single quotient type, but may be
%more convenient when the generality of {\tt define\_quotient\_types}
%is not needed.
The function {\tt define\_quotient\_types\_full\_rule}
can be defined in terms of {\tt define\_quotient\_types\_rule} as

\begin{verbatim}
fun define_quotient_types_full_rule
          {types, defs, tyop_equivs, tyop_quotients, tyop_simps,
           respects, poly_preserves, poly_respects} =
  let
      val tyop_equivs = tyop_equivs @
              [LIST_EQUIV, PAIR_EQUIV, SUM_EQUIV, OPTION_EQUIV]
      val tyop_quotients = tyop_quotients @
              [LIST_QUOTIENT, PAIR_QUOTIENT,
               SUM_QUOTIENT, OPTION_QUOTIENT, FUN_QUOTIENT]
      val tyop_simps = tyop_simps @
              [LIST_MAP_I, LIST_REL_EQ, PAIR_MAP_I, PAIR_REL_EQ,
               SUM_MAP_I, SUM_REL_EQ, OPTION_MAP_I, OPTION_REL_EQ,
               FUN_MAP_I, FUN_REL_EQ]
      val poly_preserves = poly_preserves @
              [CONS_PRS, NIL_PRS, MAP_PRS, LENGTH_PRS, APPEND_PRS,
               FLAT_PRS, REVERSE_PRS, FILTER_PRS, NULL_PRS,
               SOME_EL_PRS, ALL_EL_PRS, FOLDL_PRS, FOLDR_PRS,
               FST_PRS, SND_PRS, COMMA_PRS, CURRY_PRS,
               UNCURRY_PRS, PAIR_MAP_PRS,
               INL_PRS, INR_PRS, ISL_PRS, ISR_PRS, SUM_MAP_PRS,
               NONE_PRS, SOME_PRS, IS_SOME_PRS, IS_NONE_PRS,
               OPTION_MAP_PRS,
               FORALL_PRS, EXISTS_PRS,
               EXISTS_UNIQUE_PRS, ABSTRACT_PRS,
               COND_PRS, LET_PRS,
               I_PRS, K_PRS, o_PRS, C_PRS, W_PRS]
      val poly_respects  = poly_respects @
              [CONS_RSP, NIL_RSP, MAP_RSP, LENGTH_RSP, APPEND_RSP,
               FLAT_RSP, REVERSE_RSP, FILTER_RSP, NULL_RSP,
               SOME_EL_RSP, ALL_EL_RSP, FOLDL_RSP, FOLDR_RSP,
               FST_RSP, SND_RSP, COMMA_RSP, CURRY_RSP,
               UNCURRY_RSP, PAIR_MAP_RSP,
               INL_RSP, INR_RSP, ISL_RSP, ISR_RSP, SUM_MAP_RSP,
               NONE_RSP, SOME_RSP, IS_SOME_RSP, IS_NONE_RSP,
               OPTION_MAP_RSP,
               RES_FORALL_RSP, RES_EXISTS_RSP,
               RES_EXISTS_EQUIV_RSP, RES_ABSTRACT_RSP,
               COND_RSP, LET_RSP,
               I_RSP, K_RSP, o_RSP, C_RSP, W_RSP]
  in
    define_quotient_types_rule
          {types=types,
           defs=defs,
           tyop_equivs=tyop_equivs,
           tyop_quotients=tyop_quotients,
           tyop_simps=tyop_simps,
           respects=respects,
           poly_preserves=poly_preserves,
           poly_respects=poly_respects}
  end;
\end{verbatim}

Furthermore, two more related functions,
{\tt define\_quotient\_types\_std} and
{\tt define\_quotient\_types\_std\_rule},
are provided.
These are the same as the ``{\tt full}'' functions above, but
%do not provide
without the input record fields for
{\tt tyop\_equivs},
{\tt tyop\_quotients},
{\tt tyop\_simps},
{\tt poly\_preserves}, or
{\tt poly\_respects}.
The ``{\tt std}'' functions may be the easiest to use, providing much of the
power of higher order quotients without the need for the user
to worry about choosing theorems to include.
For many applications the ``{\tt std}'' functions will be all that is needed.

Similar to the above,
the {\tt define\_quotient\_types\_std} function
is defined in terms of {\tt define\_quotient\_types\_full} as

\begin{verbatim}
fun define_quotient_types_std {types, defs, respects, old_thms} =
    define_quotient_types_full
          {types=types, defs=defs,
           tyop_equivs=[], tyop_quotients=[],
           tyop_simps=[],
           respects=respects,
           poly_preserves=[], poly_respects=[],
           old_thms=old_thms};
\end{verbatim}

For backwards compatibility with John Harrison's excellent quotients package \cite{Har98}
%to whom much credit is due, and
(which provided much inspiration),
the following function is also provided:

\begin{verbatim}
define_equivalence_type :
        {name: string,
         equiv: thm,
         defs: {def_name: string,
                fname: string,
                func: Term.term,
                fixity: Parse.fixity} list,
         welldefs : thm list,
         old_thms : thm list} ->
        thm list
\end{verbatim}

\noindent
%This function is limited to a single quotient type, but may be
%more convenient when the generality of {\tt define\_quotient\_types}
%is not needed.
This function is defined in terms of {\tt define\_quotient\_types} as

\begin{verbatim}
fun define_equivalence_type {name,equiv,defs,welldefs,old_thms} =
    define_quotient_types
     {types=[{name=name, equiv=equiv}], defs=defs, tyop_equivs=[],
      tyop_quotients=[FUN_QUOTIENT],
      tyop_simps=[FUN_REL_EQ,FUN_MAP_I], respects=welldefs,
      poly_preserves=[FORALL_PRS,EXISTS_PRS],
      poly_respects=[RES_FORALL_RSP,RES_EXISTS_RSP],
      old_thms=old_thms};
\end{verbatim}

%\begin{verbatim}
%fun define_equivalence_type {name,equiv,defs,respects,old_thms} =
%    define_quotient_types {types=[{name=name, equiv=equiv}],
%                           defs=defs, tyop_equivs=[],
%                           tyop_quotients=[], tyop_simps=[],
%                           respects=respects, poly_preserves=[],
%                           poly_respects=[], old_thms=old_thms};
%\end{verbatim}


%
\section{New Quotient Type Definitions}
%
\label{newquotienttype}

In this section we describe how
the function {\tt define\_quotient\_types} creates new quotient types.
It automates the reasoning described
in section \ref{quotienttypes},
creating the quotient type as a new type in
the HOL logic.  It also defines the mapping functions between the
types,
forming
a quotient
%relationship
%with the equivalence relation
as described in theorem
\ref{quotientthm}.
\begin{comment}
\ref{ty_ABS_REP},
\ref{rep_respects},
and
\ref{equiv_ty_ABS}.
\end{comment}

%The new type is created by the quotient type package by internally
%making use of the HOL primitive, {\tt new\_type\_definition}.
All definitions are accomplished as definitional extensions of HOL,
and thus
preserve HOL's consistency.
%cannot introduce inconsistency.
%are completely secure.

Before invoking {\tt define\_quotient\_types}, the user should define
a relation on the original type $\tau$, and prove that it is
either 1)
an equivalence relation on the original type $\tau$, as described
in section \ref{equivalence},
%The equivalence relation should be
%expressed as a constant {\it R},
%of type
%{\tt ty -> ty -> bool}.
%$\tau_1 \rightarrow \tau_1 \rightarrow \mbox{\tt bool}$.
%If this constant is called
%In the following we will call this constant
%{\it R},
%The user should prove that {\it R\/} is indeed an equivalence relation,
as a theorem
of the form:

\begin{center}
\begin{tabular}[t]{l@{\hspace{0.3cm}}l}
{\tt R\_EQUIV} &
%{\tt |- $\forall$a b. {\it R\/} a b $\Leftrightarrow$ ({\it R\/} a = {\it R\/} b)} \\
$\vdash
(\forall x\ y.\ R\ x\ y \ \Leftrightarrow \ (R\ x = R\ y))$
\end{tabular}
\end{center}

\noindent
or 2)
that the relation is a nonempty partial equivalence relation,
%as a theorem
of the form
\begin{center}
\begin{tabular}[t]{l@{\hspace{0.3cm}}l}
{\tt R\_EQUIV} &
$\vdash
(\exists x.\ R\ x\ x) \ \wedge \
(\forall x\ y.\ R\ x\ y \ \Leftrightarrow \
                R\ x\ x \wedge R\ y\ y \wedge (R\ x = R\ y))$.
\end{tabular}
\end{center}

\noindent
Equivalently,
%the theorem
{\tt R\_EQUIV}
may be of the form
$\vdash \mbox{\tt EQUIV}\ R$
or
$\vdash \mbox{\tt PARTIAL\_EQUIV}\ R$, respectively.
These abbreviations are defined in the theorems
{\tt EQUIV\_def} and {\tt PARTIAL\_EQUIV\_def}.
Evaluating
{\tt define\_quotient\_types} with the
argument
\linebreak[4]
%field
{\tt types}
containing the record
\texttt{\{name="{\it tyname}",} {\tt equiv=R\_EQUIV\}}
automatically declares a new type {\it tyname}
in the HOL logic as the quotient type $\tau / {\it R}$,
which we will refer to from here on as $\xi$,
%with the user-specified name ``{\it tyname}'',
and
declares two new constants {\it abs} {\tt :} $\tau \rightarrow \xi$
with name ``{\it tyname}{\tt \_ABS}''
and {\it rep} {\tt :} $\xi \rightarrow \tau$
with name ``{\it tyname}{\tt \_REP}'',
such that the relation {\it R\/}
with
%respect to
{\it abs\/} and
{\it rep\/}
is a quotient,
as described in
Definition~\ref{quotientdef} of
section~\ref{quotientrelation}.
%
The {\tt define\_quotient\_types} tool proves
the quotient theorem
%for {\it R}, {\it abs}, and {\it rep},
\begin{center}
\tt
$\vdash$
QUOTIENT {\it R\/} {\it abs\/} {\it rep}
\end{center}
according to the development of
Section~\ref{quotienttypes},
and stores it in the current theory under
the automatically-generated name \mbox{\it tyname}{\tt \_QUOTIENT}.


%
\section{Lifting Definitions of Constants}
%
\label{liftingdefs}

The previous section
(\S\ref{newquotienttype})
%We have previously
dealt with lifting types across a quotient operation.
This section deals with lifting constants, including functions,
whose
types
%arguments and/or results
involve the lifted types.

Evaluating {\tt define\_quotient\_types} with the
argument
field {\tt defs}
containing the record
\begin{verse} \tt
\hspace{\parindent}
\hspace{2.0cm}
\{
def\_name = "{\it defname}", \\
\hspace{2.0cm}
fname \ \ \ = "{\it fname}", \\
\hspace{2.0cm}
func \ \ \ \ = {\it function}, \\
\hspace{2.0cm}
fixity \ \ = {\it fixity} \} \\
\end{verse}

\noindent
automatically declares a new constant {\it fname}
as a lifted version of the existing constant {\it function}.
Here {\it function} is an HOL term which is a single existing constant
of the HOL logic.
The new constant {\it fname} is given the fixity specified as {\it fixity};
this is typically {\tt Prefix}, but might be, e.g.,
{\tt Infix(NONASSOC,150)},
or some other fixity
as supported by the structure {\tt Parse}.
The definition of the new constant is stored in the current theory
under the name {\it defname}.

The theorem which is produced as the definition of the new constant
has the same form as the preservation theorems of section \ref{polypreserves},
but without antecedents.
%It is used only internally as an input to the later step of lifting theorems
%concerning this constant.  Afterwards,
After the quotient operation,
the definition theorem will not usually be of further value, as
the lifted theorems will be the basis for all further proof efforts.

Here are the values related to fixity from the structure {\tt Parse}:
\begin{verbatim}
LEFT       : associativity
RIGHT      : associativity
NONASSOC   : associativity

Infixl     : int -> fixity
Infixr     : int -> fixity
Infix      : associativity * int -> fixity
Prefix     : int -> fixity
Closefix   : fixity
Suffix     : int -> fixity
fixity     : string -> fixity
\end{verbatim}

%Here is an example of a list of definitions of lifted constants, from
%the lambda calculus:
%
%\begin{verbatim}
%      defs = [{def_name="Var_def", fname="Var",
%               func= (--`Var1`--), fixity=Prefix},
%              {def_name="App_def", fname="App",
%               func= (--`App1`--), fixity=Prefix},
%              {def_name="Lam_def", fname="Lam",
%               func= (--`Lam1`--), fixity=Prefix},
%              {def_name="HEIGHT_def", fname="HEIGHT",
%               func= (--`HEIGHT1`--), fixity=Prefix},
%              {def_name="FV_def", fname="FV",
%               func= (--`FV1`--), fixity=Prefix},
%              {def_name="SUB_def", fname="SUB",
%               func= (--`SUB1`--), fixity=Prefix},
%              {def_name="FV_subst_def", fname="FV_subst",
%               func= (--`FV_subst1`--), fixity=Prefix},
%              {def_name="SUBt_def", fname="SUBt",
%               func= (--`SUB1t`--), fixity=Prefix},
%              {def_name="vsubst_def", fname="/",
%               func= (--`$//`--), fixity=Infix(NONASSOC,150)}
%             ]
%\end{verbatim}


%
\section{Lifting Theorems of Properties}
%
\label{liftingtheorems}

Previously we have seen how to lift types, and how to lift constants
on those types.  This section describes how to lift
general theorems
%theorems of general properties
on those constants,
to restate them in terms of the lifted versions of
the constants and prove them correct,
given the existing theorems relating the lower versions of the constants.

This turns out to be a substantially more complex process than
those previously described for lifting types and functions.
Because of its difficulty, the {\tt define\_quotient\_types} tool
automates the process completely,
and greatly eases the entire task of forming quotients.
In order for the tool to work effectively and
exert its full power, several ingredients need to be provided
by the user in the form of lists of theorems that describe
key properties of the type operators and constants used
in the theorem to be lifted.  These kinds of theorems will be
described in detail in the subsections that follow.
First we
review the arguments of
{\tt define\_quotient\_types}
for lifting theorems.

\begin{verbatim}
define_quotient_types :
        {types: {name: string, equiv: thm} list,
         defs: {def_name: string, fname: string,
                func: Term.term, fixity: Parse.fixity option} list,
         tyop_equivs : thm list,
         tyop_quotients : thm list,
         tyop_simps : thm list,
         respects : thm list,
         poly_preserves : thm list,
         poly_respects : thm list,
         old_thms : thm list} ->
        thm list
\end{verbatim}

\noindent
The last four fields of the argument to {\tt define\_quotient\_types}
are lists of theorems.  The last field ({\tt old\_thms})
is the list of theorems to be lifted, and the
result produced by the tool is
the list of the lifted versions of those theorems.
The meanings of the other three fields
({\tt respects}, {\tt poly\_preserves}, {\tt poly\_respects})
are described in the following subsections.

%The theory {\tt quotientTheory} provides a number
%of theorems about the well-definedness and respectfulness of
%many common operators for lists, products, sums, options, and function types.
%These theorems ease the automation of the process of lifting theorems
%that use these common operators and
%involve the original types to their corresponding versions involving the
%quotient types.  For other operators not included, the script that
%creates the theory provides examples of how to prove such theorems,
%which is usually not difficult.


%\begin{enumerate}

%
\subsection{Respectfulness theorems: {\tt respects}}
%
\label{respectfulness}

%\item
{\tt respects} is a list of theorems demonstrating the
respectfulness of all constants used in {\tt old\_thms}
(except polymorphic operators).
These state that for each such constant,
considered as a function,
the equivalence class of the result yielded
depends only on the equivalence classes of the inputs,
not on any input's particular
value
%choice of representative
within the class.

Not all functions defined at the lower level
respect the equivalence relations involved in the
lifting process.  Theorems that mention such disrespectful functions
cannot in general be lifted.
The respectfulness of each function involved must be
demonstrated through a theorem of the general form

\begin{center}
\begin{tabular}{rl}
$\vdash$&
{\tt $\forall$(x1:$\gamma_1$) (y1:$\gamma_1$) ... (xn:$\gamma_n$) (yn:$\gamma_n$).}
\\
& \hspace{12mm}
{\tt $R_1$ x1 y1 \
$\wedge$ \
... \
$\wedge$ \
$R_n$ xn yn \;$\Rightarrow$
}  \\
& \hspace{12mm}
{\tt $R_c$ (C x1 ... xn) (C y1 ... yn)}  \\
\end{tabular}
\end{center}
where the constant {\tt C} has type
{\tt $\gamma_1$ -> ... -> $\gamma_n$ -> $\gamma_c$} ($n \ge 0$),
and each relation {\tt $R_i$} has type {\tt $\gamma_i$ -> $\gamma_i$ -> bool}
for all $i$.
Depending on the types involved,
the \quotient{} relations $R_1$, ..., $R_n$, $R_c$
may be simple equality, equivalence relations,
aggregate \quotient{} relations,
or higher-order \quotient{} relations (see section \ref{aggregates}),
as illustrated in examples below.

In fact, in the special case where one of the relations $R_i$ is simple
equality (which happens when the type
%involved
$\gamma_i$ is not a type being lifted),
the above general form may be simplified, in the following ways.
The two variables {\tt xi} and {\tt yi} may be combined into one,
say {\tt (zi:$\gamma_i$)}, e.g. in the list of universally quantified variables.
The antecedent conjunct {\tt $R_i$ xi yi}, which here is {\tt xi = yi},
may be omitted.  In the conclusion {\tt $R_c$ (C x1 ... xn) (C y1 ... yn)},
the same variable {\tt zi} may be used in place of both {\tt xi} in the first
operand of {\tt $R_c$} and {\tt yi} in the second operand.  This simpler
version is not completely standard, but may be more convenient for
the user to provide.  The package will compensate by automatically
creating the standard version from this simplified one.
Also, if all the antecedents thus simplify,
or if $n = 0$ with no antecedents,
then the implication
simplifies
%collapses
to just the consequent, {\tt $R_c$ (C z1 ... zn) (C z1 ... zn)}.

To illustrate this, the following functions are taken from an example
of syntactic terms of the untyped lambda calculus,
where the term type {\tt term1}
is being lifted to a new type {\tt term}
by identifying terms that are equivalent
according to the equivalence relation {\tt ALPHA: term1 -> term1 -> bool}.

The function {\tt Var1 : var -> term1} is used to construct
lambda calculus terms which are single variables.
The respectfulness theorem for {\tt Var1} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$x1 x2. (x1 = x2) $\Rightarrow$ ALPHA (Var1 x1) (Var1 x2)
\end{tabbing}}
\pagebreak[2]
\noindent
or possibly the simplified (but nonstandard) form
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$x. ALPHA (Var1 x) (Var1 x)
\end{tabbing}}
{\tt Var1} has one argument of type {\tt var}, which type is not lifted,
so the \quotient{} relation of this argument is simple equality.
The result type is {\tt term1}, so the \quotient{} relation for the
result is {\tt ALPHA}.

The function {\tt App1 : term1 -> term1 -> term1}
is used to construct terms which are applications of a function to an argument.
The respectfulness theorem for {\tt App1} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$t\=1 t2 u1 u2. \\
\>       ALPHA t1 t2 $\wedge$ ALPHA u1 u2 $\Rightarrow$\\
\>       ALPHA (App1 t1 u1) (App1 t2 u2)
\end{tabbing}}
{\tt App1} has two arguments.
The first argument has type {\tt term1},
so the \quotient{} relation of this argument is {\tt ALPHA}.
The second argument also has type {\tt term1},
so the \quotient{} relation of this argument is also {\tt ALPHA}.
The result type is {\tt term1}, so the \quotient{} relation for the
result is {\tt ALPHA}.

The function {\tt HEIGHT1 : term1 -> num}
is used to calculate the height of a term as a tree.
The respectfulness theorem for {\tt HEIGHT1} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$t1 t2. ALPHA t1 t2 $\Rightarrow$ (HEIGHT1 t1 = HEIGHT1 t2)
\end{tabbing}}
{\tt HEIGHT1} has one argument, which
has type {\tt term1},
so the \quotient{} relation of the argument is {\tt ALPHA}.
The result type is {\tt num}, which is not being lifted,
so the \quotient{} relation for the result is simple equality.

The function {\tt FV1 : term1 -> (var -> bool)}
is used to calculate the set of free variables of a term.
The respectfulness theorem for {\tt FV1} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$t1 t2. ALPHA t1 t2 $\Rightarrow$ (FV1 t1 = FV1 t2)
\end{tabbing}}
{\tt FV1} has one argument, which
has type {\tt term1},
so the \quotient{} relation of the argument is {\tt ALPHA}.
The result type is {\tt var -> bool}.
Even though this is a functional type,
it is not affected by lifting,
so the \quotient{} relation for the result is simple equality.

The function {\tt <[ : term1 -> (var \# term1) list -> term1}
is used to simultaneously substitute a list of terms
for a corresponding list of variables
where they occur free across a target term.
The respectfulness theorem for {\tt <[} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$t\=1 t2 s1 s2. \\
\>       ALPHA t1 t2 $\wedge$ LIST\_REL (\$= \#\#\# ALPHA) s1 s2 $\Rightarrow$ \\
\>       ALPHA (t1 <[ s1) (t2 <[ s2)
\end{tabbing}}
{\tt <[} has two arguments.
The first argument has type {\tt term1},
so the \quotient{} relation of this argument is {\tt ALPHA}.
The second argument is a substitution, which has type {\tt (var \# term1) list},
so the \quotient{} relation of this argument is {\tt LIST\_REL (\$= \#\#\# ALPHA)}.
The result type is {\tt term1}, so the \quotient{} relation for the
result is {\tt ALPHA}.

%Consider the following nine functions, taken from an example of terms of the
%lambda calculus, where the term type {\tt term1} is being lifted to a new
%type {\tt term} according to the equivalence relation
%{\tt ALPHA: term1 -> term1 -> bool}.
%\begin{center}
%{\tt
%\begin{tabular}{lcl}
%Var1       & : & var -> term1 \\
%App1       & : & term1 -> term1 -> term1 \\
%Lam1       & : & var -> term1 -> term1 \\
%HEIGHT1    & : & term1 -> num \\
%FV1        & : & term1 -> (var -> bool) \\
%SUB1       & : & (var \# term1) list -> var -> term1 \\
%FV\_subst1 & : & (var \# term1) list -> (var -> bool) -> (var -> bool) \\
%\$//       & : & var list -> var list -> (var \# term1) list \\
%\$<[       & : & term1 -> (var \# term1) list -> term1 \\
%\end{tabular}
%}
%\end{center}
%
%\noindent
%Then the following nine theorems show the respectfulness of these functions:
%\begin{verbatim}
%    |- !x1 x2. (x1 = x2) ==> ALPHA (Var1 x1) (Var1 x2)
%    |- !t1 t2 u1 u2.
%         ALPHA t1 t2 /\ ALPHA u1 u2
%         ==> ALPHA (App1 t1 u1) (App1 t2 u2)
%    |- !x1 x2 t1 t2.
%         (x1 = x2) /\ ALPHA t1 t2
%         ==> ALPHA (Lam1 x1 t1) (Lam1 x2 t2)
%    |- !t1 t2. ALPHA t1 t2 ==> (HEIGHT1 t1 = HEIGHT1 t2)
%    |- !t1 t2. ALPHA t1 t2 ==> (FV1 t1 = FV1 t2)
%    |- !s1 s2 x1 x2.
%         LIST_REL ($= ### ALPHA) s1 s2 /\ (x1 = x2) ==>
%         ALPHA (SUB1 s1 x1) (SUB1 s2 x2)
%    |- !s1 s2 xs ys.
%         LIST_REL ($= ### ALPHA) s1 s2 /\ (xs = ys) ==>
%         (FV_subst1 s1 xs = FV_subst1 s2 ys)
%    |- !xs1 xs2 ys1 ys2.
%         (xs1 = xs2) /\ (ys1 = ys2) ==>
%         LIST_REL ($= ### ALPHA) (xs1 // ys1) (xs2 // ys2)
%    |- !t1 t2 s1 s2.
%         ALPHA t1 t2 /\ LIST_REL ($= ### ALPHA) s1 s2 ==>
%         ALPHA (t1 <[ s1) (t2 <[ s2)
%\end{verbatim}

%val respects = [Var1_ALPHA, App1_ALPHA, Lam1_ALPHA, ALPHA_HEIGHT,
%                ALPHA_FV, SUB1_RSP, FV_subst_RSP, vsubst1_RSP, SUBt_RSP]
%
% \begin{verbatim}
% > val respects =
%     [|- !x1 x2. (x1 = x2) ==> ALPHA (Var1 x1) (Var1 x2),
%      |- !t1 t2 u1 u2.
%           ALPHA t1 t2 /\ ALPHA u1 u2 ==>
%           ALPHA (App1 t1 u1) (App1 t2 u2),
%      |- !x1 x2 t1 t2.
%           (x1 = x2) /\ ALPHA t1 t2 ==>
%           ALPHA (Lam1 x1 t1) (Lam1 x2 t2),
%      |- !t1 t2. ALPHA t1 t2 ==> (HEIGHT1 t1 = HEIGHT1 t2),
%
%      |- !t1 t2. ALPHA t1 t2 ==> (FV1 t1 = FV1 t2),
%      |- !s1 s2 x1 x2.
%           LIST_REL ($= ### ALPHA) s1 s2 /\ (x1 = x2) ==>
%           ALPHA (SUB1 s1 x1) (SUB1 s2 x2),
%      |- !s1 s2 xs ys.
%           LIST_REL ($= ### ALPHA) s1 s2 /\ (xs = ys) ==>
%           (FV_subst1 s1 xs = FV_subst1 s2 ys),
%      |- !xs1 xs2 ys1 ys2.
%           (xs1 = xs2) /\ (ys1 = ys2) ==>
%           LIST_REL ($= ### ALPHA) (xs1 // ys1) (xs2 // ys2),
%      |- !t1 t2 s1 s2.
%           ALPHA t1 t2 /\ LIST_REL ($= ### ALPHA) s1 s2 ==>
%           ALPHA (t1 <[ s1) (t2 <[ s2)] : thm list
% \end{verbatim}

% These nine theorems show the respectfulness of the functions
% {\tt Var1}, {\tt App1},
% {\tt Lam1}, {\tt HEIGHT1},
% {\tt FV1}, {\tt SUB1},
% {\tt FV\_subst1},
% {\tt //}, and {\tt <[}.

Please note how the antecedents of each theorem relate to the arguments
of the function.  The arguments which have types not being lifted
are compared by equality, while the arguments which have types being lifted
are compared by the corresponding \quotient{} relation.  Similarly, the
consequent of each of the theorems above is either a \quotient{} or an
equality, depending on whether the type of the value returned by the
function is of a type being lifted or not.  There is a direct one-to-one
relationship between the type of the argument/result and the
\quotient{} relation used to compare its values.

Therefore the antecedent of the theorem on the respectfulness of {\tt Var1}
is an equality, since the type of the argument is {\tt var} which is not
being lifted, while the antecedents of the theorem on the respectfulness
of {\tt App1} are both \quotient{}s, since the type of those arguments is
{\tt term1}, which is being lifted according to the equivalence relation
{\tt ALPHA}.  Also, the consequent of the theorem on the respectfulness
of {\tt HEIGHT1} is an equality, since the type of the value returned
by {\tt HEIGHT1} is {\tt num}, which is not being lifted.  If the
arguments and the value returned by a function are all of types
not being lifted, then there is no need for a respectfulness theorem
for that function.

Also, where a function has an argument of an aggregate type,
the corresponding \quotient{} relation is created by an aggregate operator.
For example, in the theorem on the respectfulness of
{\tt <[}, the
%second argument has type
type of the second argument is
{\tt (var \# term1) list}.
The
\quotient{}
relation that corresponds to this type is
{\tt LIST\_REL (\$= \#\#\# ALPHA)},
constructed by first
using the {\tt \#\#\#} operator to create the
%\quotient{}
relation for
{\tt var \# term1},
and then using the {\tt LIST\_REL}
operator to create the
%\quotient{}
relation for
{\tt (var \# term1) list}.
These \quotient{} relation operators
are described in section \ref{aggregates}.

Whenever there are arguments to the constant, there are
multiple equivalent ways to state the respectfulness theorem.
For example, the respectfulness theorem for {\tt FV1:term1 -> var -> bool} may be given
equally well as any of the following completely equivalent versions:
{\tt \begin{tabbing}
\hspace{5.5mm}
    \=$\vdash \forall$t\=1 t2 x1 x2. \\
\>\>     ALPHA t1 t2 $\wedge$ (x1 = x2) $\Rightarrow$ (FV1 t1 x1 = FV1 t2 x2) \\
\>  $\vdash \forall$t1 t2. ALPHA t1 t2 $\Rightarrow$ (FV1 t1 = FV1 t2) \\
\>  $\vdash$ (ALPHA ===> \$=) FV1 FV1
\end{tabbing}}
The last version has higher order and lesser arity than the
earlier versions.  In fact, the three theorems above have arities
2, 1, and 0, respectively,
while the last theorem is the only one with a
higher order \quotient{} relation.
The earlier versions may be easier to understand and prove than the
last version.  For the quotient package's internal use, all respectfulness
theorems are automatically converted to the highest order and lowest
arity possible, usually with arity zero.


%
\subsection{
Preservation
%``Definitions''
of polymorphic functions: {\tt poly\_preserves}}
%
\label{polypreserves}

%\item
{\tt poly\_preserves} is a list of theorems expressing the preservation
of generic, polymorphic functions across quotient operations.
%such as {\tt NIL}, {\tt LENGTH}, {\tt CONS}, {\tt FST}, and {\tt o}.
This is expressed as an
equality between the value of the function applied to arguments of
lifted types, and the lifted version of the value of the same function
applied to arguments of the lower types.
The equalities are conditioned on the component types being quotients.

These preservation theorems have the following general form.
\begin{center}
\begin{tabular}{rl}
$\vdash$
& {\tt $\forall$R1 (abs1:$\alpha_1$->$\beta_1$) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$} \\
& {\tt ...} \\
& {\tt $\forall$Rn (absn:$\alpha_n$->$\beta_n$) repn. QUOTIENT Rn absn repn $\Rightarrow$} \\
& {\tt $\forall$(x1:$\delta_1$) ... (xk:$\delta_k$).}  \\
& \hspace{17mm}
{\tt C' x1 ... xk = $abs_c$ (C ($rep_1$ x1) ... ($rep_k$ xk)) }  \\
\end{tabular}
\end{center}
where
\begin{enumerate}
\item
the constant {\tt C} has a polymorphic type with $n>0$ type variables,
$\alpha_1, ..., \alpha_n$,
%where $n > 0$,
% and where
\item
{\tt C'} is usually {\tt C}, but may be a different constant
in case {\tt C} is not preserved,
% and where
\item
the type of {\tt C} is of the form
{\tt $\gamma_1$ -> ... -> $\gamma_k$ -> $\gamma_c$} ($k \ge 0$) \\
({\tt C} is a curried function of $k$ arguments, with a return value of
type $\gamma_c$), \\
with
all type variables in the $\gamma_1$, ..., $\gamma_k$, $\gamma_c$ types
contained within $\alpha_1$,~...,~$\alpha_n$,
% and where
\item
the type of {\tt C'} is of the form
{\tt $\delta_1$ -> ... -> $\delta_k$ -> $\delta_c$} ($k \ge 0$) \\
({\tt C'} is a curried function of $k$ arguments, with a return value of
type $\delta_c$),
% and where
\item
$\delta_i$ is the lifted version of $\gamma_i$ for all $i=1,...,k,c$ \\
($\delta_i = \gamma_i[\alpha_j \mapsto \beta_j \mbox{\ for all\ } j=1,...,n]$),
%($\delta_i = \gamma_i[\alpha_i \mapsto \beta_i \forall i=1,...,n]$),
\\
with
all type variables in the $\delta_1$, ..., $\delta_k$, $\delta_c$ types
contained within $\beta_1$,~...,~$\beta_n$,
and
\item
{\tt $abs_i$:$\gamma_i$ -> $\delta_i$} and
{\tt $rep_i$:$\delta_i$ -> $\gamma_i$}
are the (possibly identity, aggregate, or higher-order)
abstraction and representation functions
for the type $\gamma_i$, for all $i=1,...,k,c$.
These are expressions, not simply an
{\tt absi} or {\tt repi} variable.
\end{enumerate}

Depending on the types involved, some
of the abstraction or representation functions
%{\tt absj}, {\tt repj}, ..., {\tt Rk}, {\tt Rt}
may be the identity function {\tt I}, in which case they disappear,
as illustrated in some of the examples below.

For clarity, we will discuss examples for particular polymorphic operators,
beginning with simpler ones.
In each case, the main driver of the form of the resulting theorem is the
the operator's type, in particular the number of arguments, the type of
each argument, and the type returned by the operator.

The preservation theorem for {\tt NIL} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$R (a\=bs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\
\>          ([] = MAP abs [])
\end{tabbing}}
The operator {\tt NIL} has polymorphic type {\tt ('a)list}.
It has one type variable, {\tt 'a}, so $n = 1$.
It has no arguments, so $k = 0$.
The result type is
%$\gamma_c$ =
{\tt ('a)list},
%The lifted version of this type is
%$\delta_c$ = {\tt ('b)list}.
for which
the abstraction function
%for $\gamma_c$
is {\tt MAP abs}.

\pagebreak[2]
The preservation theorem for {\tt LENGTH} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$R\=\ (abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\
\>       $\forall$l. LENGTH l = LENGTH (MAP rep l)
\end{tabbing}}
The operator {\tt LENGTH} has polymorphic type {\tt ('a)list -> num}.
It has one type variable, {\tt 'a}, so $n = 1$.
It has one argument, so $k = 1$.
The argument type is
%$\gamma_1$ =
{\tt ('a)list},
for which
the representation function
%for $\gamma_1$
is {\tt MAP rep}.
The result type is
%$\gamma_c$ =
{\tt num},
for which
%The lifted versions of these types are
%$\delta_1$ = {\tt ('b)list},
%$\delta_c$ = {\tt num}.
the abstraction function
%for $\gamma_c$
is {\tt I}, which disappears.

\pagebreak[2]
The preservation theorem for {\tt CONS} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$R\=\ (abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\
\>       $\forall$t h. h::t = MAP abs (rep h::MAP rep t)
\end{tabbing}}
The operator {\tt CONS} has polymorphic type {\tt 'a -> ('a)list -> ('a)list}.
It has one type variable, {\tt 'a}, so $n = 1$.
It has two arguments, so $k = 2$.
The first argument type is
%$\gamma_1$ =
{\tt 'a},
for which
the representation function
%for $\gamma_1$
is {\tt rep}.
The second argument type is
%$\gamma_2$ =
{\tt ('a)list},
for which
the representation function
%for $\gamma_2$
is {\tt MAP rep}.
The result type is
%$\gamma_c$ =
{\tt ('a)list},
for which
the abstraction function
%for $\gamma_c$
is {\tt MAP abs}.
%The lifted versions of these types are
%$\delta_1$ = {\tt 'b},
%$\delta_2$ = {\tt ('b)list},
%$\delta_c$ = {\tt ('b)list}.

The preservation theorem for {\tt FST} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash$ \=$\forall$R\=1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\
\>     $\forall$R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\
\>\>     $\forall$p:'c \# 'd. FST p = abs1 (FST ((rep1 \#\# rep2) p))
\end{tabbing}}
The operator {\tt FST} has polymorphic type {\tt ('a \# 'b) -> 'a}.
It has two type variables, {\tt 'a} and {\tt 'b}, so $n = 2$.
It has one argument, so $k = 1$.
The argument type is
%$\gamma_1$ =
{\tt ('a \# 'b)},
for which
the representation function
%for $\gamma_1$
is {\tt rep1 \#\# rep2}.
The result type is
%$\gamma_c$ =
{\tt 'a},
for which
the abstraction function
%for $\gamma_c$
is {\tt abs1}.
%The lifted versions of these types are
%$\delta_1$ = {\tt ('c \# 'd)},
%$\delta_c$ = {\tt 'c}.

\pagebreak[3]
The preservation theorem for the composition operator {\tt o} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash$ \=$\forall$R\=1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\
\>     $\forall$R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\
\>     $\forall$R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 $\Rightarrow$ \\
\>\>     $\forall$f\=\ g. f o g = \\
\>\>\>     (rep1 --> abs3) ((abs2 --> rep3) f o (abs1 --> rep2) g)
\end{tabbing}}
The operator {\tt o} has type
{\tt ('b ->\;'c) -> ('a ->\;'b) -> ('a ->\;'c)},
which is polymorphic and also higher order.
It has three type variables, {\tt 'a}, {\tt 'b}, and {\tt 'c}, so $n = 3$.
It has two arguments, so $k = 2$.
The first argument type is
%$\gamma_1$ =
{\tt 'b -> 'c},
for which
the representation function
%for $\gamma_1$
is {\tt abs2 --> rep3}.
The second argument type is
%$\gamma_2$ =
{\tt 'a -> 'b},
for which
the representation function
%for $\gamma_2$
is {\tt abs1 --> rep2}.
The result type is
%$\gamma_c$ =
{\tt 'a -> 'c},
for which
the abstraction function
%for $\gamma_c$
is {\tt rep1 --> abs3}.
%The lifted versions of these types are
%$\delta_1$ = {\tt 'e -> 'f},
%$\delta_1$ = {\tt 'd -> 'e},
%$\delta_c$ = {\tt 'd -> 'f}.

%Because the operator {\tt o} returns a higher-order result, the operator
%could be considered to have three arguments, not two, where the type of
%the third argument is {\tt 'a}, for which the representation function
%is {\tt rep1}, and where the result type is {\tt 'c}, for which the
%abstraction function is {\tt abs3}.  This choice would give rise to
%the following variant definition theorem.  Either choice is fine.
%\begin{verbatim}
%    |- !R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
%       !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
%       !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
%         !f g x. (f o g) x =
%           abs3 (((abs2 --> rep3) f o (abs1 --> rep2) g) (rep1 x))
%\end{verbatim}


Since the types of
these functions are polymorphic, instances of the functions may be applied
on arguments of either the types being lifted or the higher, lifted types.
In a style very similar to the definition theorems constructed
by {\tt define\_quotient\_types} for the new versions of the
constants being lifted,
each theorem expresses that the value of
the operator applied to arguments of the lifted types
is equal to the lifted version of the value of the same operator
applied to arguments of the lower types,
computed by lowering the original arguments.

So for example, in the {\tt CONS} example above,
the {\tt CONS} operator is equal to taking its arguments
{\tt h} and {\tt t}, lowering each argument as {\tt rep h} and {\tt MAP rep t},
then applying {\tt CONS} to these two lowered arguments to compute the
result at the lower level, and then raising the result to the lifted level
by {\tt MAP abs}.

These
express the use of each polymorphic function at the
lifted level in terms of its use at the lower level.

These theorems differ from
the definition theorems for new constants
is that each theorem conditions the preservation statement
upon the polymorphic types being
proper quotients.  The conditions follow the form
of a quotient theorem as given in section \ref{newquotienttype},
but each describes a quotient for a polymorphic type variable
instead of for a specific type.  If the function is polymorphic in more
than one type, then the theorem will be conditioned on all of the
type variables being quotient types.

Thus in the {\tt o} example above, the preservation
of the composition operator {\tt o}
is conditioned on three types being lifted,
where {\tt 'a} is being lifted to {\tt 'd},
{\tt 'b} is being lifted to {\tt 'e}, and
{\tt 'c} is being lifted to {\tt 'f}.
This calls for three antecedents which are quotient theorems of {\tt 'a},
{\tt 'b}, and {\tt 'c}.
In a theorem to be lifted, when
the composition operator is actually applied
to arguments which are functions from specific domains
to specific ranges, the {\tt o} preservation theorem will be
instantiated with those types,
to be resolved against actual quotient theorems for those types.

A substantial collection of these
preservation
%``definition''
theorems for various
standard polymorphic functions of the HOL logic have been proven already and
is available in the theories of the quotient library (see Table 1).
If there is a need to use a
polymorphic function not covered by these, the corresponding
preservation
%``definition''
theorem can be proven by the user, using the same approach as for the example
theorems above, as shown in the theory scripts of the quotient library.

Whenever there are arguments to the constant, there are
multiple equivalent ways to state the
preservation
%``definition''
theorem.
For example, the consequent of the
preservation
%``definition''
theorem for {\tt o}
may be given
equally well as any of the following completely equivalent versions:
\pagebreak[2]
{\tt \begin{tabbing}
$\forall$f g x. (\=f o g) x = \\
\>       abs3 (((abs2 --> rep3) f o (abs1 --> rep2) g) (rep1 x)) \\
$\forall$f g. \=f o g = \\
\>    (rep1 --> abs3) ((abs2 --> rep3) f o (abs1 --> rep2) g) \\
$\forall$f. \=\$o f = \\
\>  ((abs1 --> rep2) --> (rep1 --> abs3)) (\$o ((abs2 --> rep3) f)) \\
\$o = ((abs2 --> rep3) --> (abs1 --> rep2) --> (rep1 --> abs3)) \$o
\end{tabbing}}
In each of the versions, the type of the {\tt \$o} on the left hand side
of the equality
is {\tt ('e -> 'f) -> ('d -> 'e) -> ('d -> 'f)},
while the type of the {\tt \$o} on the right hand side
is {\tt ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)}.
The last version has higher order and lesser arity than the
earlier versions.  In fact, the four versions above have arities
3, 2, 1, and 0, respectively.
The earlier versions may be easier to understand and prove than the
last version.
For the quotient package's internal use, all preservation
theorems are automatically converted to the lowest order and highest
arity possible, and then all higher order versions are produced
% The entire collection of versions is
and used for lifting theorems
which involve the operator.

\vfill

\begin{table}
\begin{center}
{\bfseries TABLE 1.\\
Preservation
%Definition
and Respectfulness Theorems for Polymorphic Operators}\\[1ex]
\begin{tabular}{|lll|l|l|}
\hline
\multicolumn{3}{|l|}
{Lifted Operators} &
%Lifted
Preservation
%Definition
Theorems & Respectfulness Theorems \\
\hline
{\tt $\forall$\_::\_.\_} & $\rightarrow$ & {\tt $\forall$\_.\_} & {\tt FORALL\_PRS} & {\tt RES\_FORALL\_RSP} \\
{\tt $\exists$\_::\_.\_} & $\rightarrow$ & {\tt $\exists$\_.\_} & {\tt EXISTS\_PRS} & {\tt RES\_EXISTS\_RSP} \\
{\tt $\exists !!$\_::\_.\_} & $\rightarrow$ & {\tt $\exists !$\_.\_}
& {\tt EXISTS\_UNIQUE\_PRS} & {\tt RES\_EXISTS\_EQUIV\_RSP} \\
% {\tt \verb+\+\_.\_} & & & {\tt LAMBDA\_PRS} & {\tt LAMBDA\_RSP} \\
%{\tt \verb+\+\_::\_.\_} & $\rightarrow$ & {\tt \verb+\+\_.\_}
{\tt $\lambda$\_::\_.\_} & $\rightarrow$ & {\tt $\lambda$\_.\_}
& {\tt ABSTRACT\_PRS} & {\tt RES\_ABSTRACT\_RSP} \\
{\tt COND} & & & {\tt COND\_PRS} & {\tt COND\_RSP} \\
{\tt LET} & & & {\tt LET\_PRS} & {\tt LET\_RSP} \\
{\tt FST} & & & {\tt FST\_PRS} & {\tt FST\_RSP} \\
{\tt SND} & & & {\tt SND\_PRS} & {\tt SND\_RSP} \\
{\tt ,} & & & {\tt COMMA\_PRS} & {\tt COMMA\_RSP} \\
{\tt CURRY} & & & {\tt CURRY\_PRS} & {\tt CURRY\_RSP} \\
{\tt UNCURRY} & & & {\tt UNCURRY\_PRS} & {\tt UNCURRY\_RSP} \\
{\tt \#\#} & & & {\tt PAIR\_MAP\_PRS} & {\tt PAIR\_MAP\_RSP} \\
{\tt INL} & & & {\tt INL\_PRS} & {\tt INL\_RSP} \\
{\tt INR} & & & {\tt INR\_PRS} & {\tt INR\_RSP} \\
{\tt ISL} & & & {\tt ISL\_PRS} & {\tt ISL\_RSP} \\
{\tt ISR} & & & {\tt ISR\_PRS} & {\tt ISR\_RSP} \\
{\tt ++} & & & {\tt SUM\_MAP\_PRS} & {\tt SUM\_MAP\_RSP} \\
{\tt CONS} & & & {\tt CONS\_PRS} & {\tt CONS\_RSP} \\
{\tt NIL} & & & {\tt NIL\_PRS} & {\tt NIL\_RSP} \\
{\tt MAP} & & & {\tt MAP\_PRS} & {\tt MAP\_RSP} \\
{\tt LENGTH} & & & {\tt LENGTH\_PRS} & {\tt LENGTH\_RSP} \\
{\tt APPEND} & & & {\tt APPEND\_PRS} & {\tt APPEND\_RSP} \\
{\tt FLAT} & & & {\tt FLAT\_PRS} & {\tt FLAT\_RSP} \\
\multicolumn{3}{|l|}
{\tt REVERSE} & {\tt REVERSE\_PRS} & {\tt REVERSE\_RSP} \\
{\tt FILTER} & & & {\tt FILTER\_PRS} & {\tt FILTER\_RSP} \\
{\tt NULL} & & & {\tt NULL\_PRS} & {\tt NULL\_RSP} \\
{\tt SOME\_EL} & & & {\tt SOME\_EL\_PRS} & {\tt SOME\_EL\_RSP} \\
{\tt ALL\_EL} & & & {\tt ALL\_EL\_PRS} & {\tt ALL\_EL\_RSP} \\
{\tt FOLDL} & & & {\tt FOLDL\_PRS} & {\tt FOLDL\_RSP} \\
{\tt FOLDR} & & & {\tt FOLDR\_PRS} & {\tt FOLDR\_RSP} \\
{\tt NONE} & & & {\tt NONE\_PRS} & {\tt NONE\_RSP} \\
{\tt SOME} & & & {\tt SOME\_PRS} & {\tt SOME\_RSP} \\
{\tt IS\_SOME} & & & {\tt IS\_SOME\_PRS} & {\tt IS\_SOME\_RSP} \\
{\tt IS\_NONE} & & & {\tt IS\_NONE\_PRS} & {\tt IS\_NONE\_RSP} \\
{\tt OPTION\_MAP} & & & {\tt OPTION\_MAP\_PRS} & {\tt OPTION\_MAP\_RSP} \\
% function application & & & {\tt APPLY\_PRS} & {\tt APPLY\_RSP} \\
%\multicolumn{3}{|l|}
%{{\tt I}, {\tt K}, {\tt o}, {\tt C}, {\tt W}}
%& {\tt I\_PRS}, {\tt K\_PRS}, {\tt o\_PRS}, etc. \
%& {\tt I\_RSP}, {\tt K\_RSP}, {\tt o\_RSP}, etc. \\
{\tt I} & & & {\tt I\_PRS} & {\tt I\_RSP} \\
{\tt K} & & & {\tt K\_PRS} & {\tt K\_RSP} \\
{\tt o} & & & {\tt o\_PRS} & {\tt o\_RSP} \\
{\tt C} & & & {\tt C\_PRS} & {\tt C\_RSP} \\
{\tt W} & & & {\tt W\_PRS} & {\tt W\_RSP}
\begin{comment}
{\tt IN} & & & {\tt IN\_PRS} & {\tt IN\_RSP} \\
{\tt EMPTY} & & & {\tt EMPTY\_PRS} & {\tt EMPTY\_RSP} \\
{\tt UNIV} & & & {\tt UNIV\_PRS} & {\tt UNIV\_RSP} \\
\multicolumn{3}{|l|}{{\tt INTER}, {\tt UNION}}
  & {\tt INTER\_PRS}, {\tt UNION\_PRS} & {\tt INTER\_RSP}, {\tt UNION\_RSP} \\
%{\tt INTER} & & & {\tt INTER\_PRS} & {\tt INTER\_RSP} \\
%{\tt UNION} & & & {\tt UNION\_PRS} & {\tt UNION\_RSP} \\
{\tt SUBSETR} & $\rightarrow$ & {\tt SUBSET}
& {\tt SUBSET\_PRS} & {\tt SUBSETR\_RSP} \\
{\tt PSUBSETR} & $\rightarrow$ & {\tt PSUBSET}
& {\tt PSUBSET\_PRS} & {\tt PSUBSETR\_RSP} \\
{\tt IMAGER} & $\rightarrow$ & {\tt IMAGE}
& {\tt IMAGE\_PRS} & {\tt IMAGER\_RSP} \\
\end{comment}
\\
\hline
\end{tabular}
\\
\end{center}
An arrow
({\it lower} $\rightarrow$ {\it higher})
indicates that in
preservation theorems,
%definition,
the lower operator
is different
%differs
from the higher,
%otherwise
else
it
%the operator
is the same.
%\\
Respectfulness theorems concern
{\it lower}.
%the lower operator.
\end{table}

%
\subsection{Respectfulness of polymorphic functions: {\tt poly\_respects}}
%
\label{polyrespects}

%\item
{\tt poly\_respects} is a list of theorems expressing the
respectfulness of generic, polymorphic functions.
%such as {\tt CONS}, {\tt LENGTH}, {\tt FST}, {\tt I}, or {\tt o}.

Since the types of
these functions are polymorphic, instances of the functions may be applied
to arguments of the types being lifted.
%or the higher, lifted types.
Each theorem expresses
that an operator respects the \quotient{} relations involved, just as
for the {\tt respects} field (\S\ref{respectfulness}),
except that the theorem conditions
the respectfulness of the operator upon the polymorphic types being
quotients.  The conditioning is the same as that described
in the previous section
for {\tt poly\_preserves} (\S\ref{polypreserves}).

These theorems have the following general form.
\begin{center}
\begin{tabular}{rl}
$\vdash$
& {\tt $\forall$R1 (abs1:$\alpha_1$->$\beta_1$) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$} \\
& {\tt ...} \\
& {\tt $\forall$Rn (absn:$\alpha_n$->$\beta_n$) repn. QUOTIENT Rn absn repn $\Rightarrow$} \\
& {\tt $\forall$(x1:$\gamma_1$) (y1:$\gamma_1$) ... (xk:$\gamma_k$) (yk:$\gamma_k$).}
\\
& \hspace{12mm}
{\tt $R_1$ x1 y1 \
$\wedge$ \
... \
$\wedge$ \
$R_k$ xk yk $\Rightarrow$
}  \\
& \hspace{12mm}
{\tt $R_c$ (C x1 ... xk) (C y1 ... yk)}  \\
\end{tabular}
\end{center}
where
\begin{enumerate}
\item
the constant {\tt C} has a polymorphic type with $n$ type variables,
$\alpha_1, ..., \alpha_n$,
\item
$\beta_1, ..., \beta_n$ are $n$ other type variables,
% and where
\item
the type of {\tt C} is of the form
{\tt $\gamma_1$ -> ... -> $\gamma_k$ -> $\gamma_c$} \\
({\tt C} is a curried function of $k$ arguments, with a return value of
type $\gamma_c$), \\
with
all type variables in the $\gamma_1$, ..., $\gamma_k$, $\gamma_c$ types
contained within $\alpha_1$,~...,~$\alpha_n$,
and
\item
{\tt $R_i$:$\gamma_i$ -> $\gamma_i$ -> bool}
is the (possibly equality, aggregate, or higher-order)
\quotient{} relation
for the type $\gamma_i$, for all $i=1,...,k,c$.
This is an expression, not simply an
{\tt Ri} variable.
\end{enumerate}

For clarity, we will discuss examples for particular polymorphic
operators, beginning with simpler ones.  In each case, the main driver
of the form of the resulting theorem is the operator's type,
in particular the number of arguments, the type of each, and the type
returned by the operator.

\pagebreak[3]
The respectfulness theorem for {\tt NIL} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$R\=\ (abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\
\>       LIST\_REL R [] []
\end{tabbing}}
The operator {\tt NIL} has polymorphic type {\tt ('a)list}.
It has one type variable, {\tt 'a}, so $n = 1$.
It has no arguments, so $k = 0$.
The result type is
%$\gamma_c$ =
{\tt ('a)list},
%The lifted version of this type is
%$\delta_c$ = {\tt ('b)list}.
for which
the \quotient{} relation
%for $\gamma_c$
is {\tt LIST\_REL R}.

\pagebreak[2]
The respectfulness theorem for {\tt LENGTH} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$R\=\ (abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\
\>       $\forall$l1 l2. \=LIST\_REL R l1 l2 $\Rightarrow$ \\
\>\>             (LENGTH l1 = LENGTH l2)
\end{tabbing}}
The operator {\tt LENGTH} has polymorphic type {\tt ('a)list -> num}.
It has one type variable, {\tt 'a}, so $n = 1$.
It has one argument, so $k = 1$.
The argument type is
%$\gamma_1$ =
{\tt ('a)list},
for which
the \quotient{} relation
%for $\gamma_1$
is {\tt LIST\_REL R}.
The result type is
%$\gamma_c$ =
{\tt num},
for which
the \quotient{} relation
%for $\gamma_c$
is {\tt =}.
%The lifted versions of these types are
%$\delta_1$ = {\tt ('b)list},
%$\delta_c$ = {\tt num}.

The respectfulness theorem for {\tt CONS} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$R\=\ (abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\
\>       $\forall$t\=1 t2 h1 h2. \\
\>\>       R h1 h2 $\wedge$ LIST\_REL R t1 t2 $\Rightarrow$ \\
\>\>       LIST\_REL R (h1::t1) (h2::t2)
\end{tabbing}}
The operator {\tt CONS} has polymorphic type {\tt 'a -> ('a)list -> ('a)list}.
It has one type variable, {\tt 'a}, so $n = 1$.
It has two arguments, so $k = 2$.
The first argument type is
%$\gamma_1$ =
{\tt 'a},
for which
the \quotient{} relation
%for $\gamma_1$
is {\tt R}.
The second argument type is
%$\gamma_2$ =
{\tt ('a)list},
for which
the \quotient{} relation
%for $\gamma_2$
is {\tt LIST\_REL R}.
The result type is
%$\gamma_c$ =
{\tt ('a)list},
for which
the \quotient{} relation
%for $\gamma_c$
is {\tt LIST\_REL R}.
%The lifted versions of these types are
%$\delta_1$ = {\tt 'b},
%$\delta_2$ = {\tt ('b)list},
%$\delta_c$ = {\tt ('b)list}.

The respectfulness theorem for {\tt FST} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash$ \=$\forall$R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\
\>     $\forall$R\=2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\
\>\>     $\forall$p1 p2. \=(R1 \#\#\# R2) p1 p2 $\Rightarrow$ \\
\>\>\>           R1 (FST p1) (FST p2)
\end{tabbing}}
The operator {\tt FST} has polymorphic type {\tt ('a \# 'b) -> 'a}.
It has two type variables, {\tt 'a} and {\tt 'b}, so $n = 2$.
It has one argument, so $k = 1$.
The argument type is
%$\gamma_1$ =
{\tt ('a \# 'b)},
for which
the \quotient{} relation
%for $\gamma_1$
is {\tt R1 \#\#\# R2}.
The result type is
%$\gamma_c$ =
{\tt 'a},
for which
the \quotient{} relation
%for $\gamma_c$
is {\tt R1}.
%The lifted versions of these types are
%$\delta_1$ = {\tt ('c \# 'd)},
%$\delta_c$ = {\tt 'c}.

The respectfulness theorem for the composition operator {\tt o} is
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash$ \=$\forall$R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\
\>     $\forall$R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\
\>     $\forall$R\=3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 $\Rightarrow$ \\
\>\>     $\forall$f\=1 f2 g1 g2. \\
\>\>\>     (R2 ===> R3) f1 f2 $\wedge$ (R1 ===> R2) g1 g2 $\Rightarrow$ \\
\>\>\>     (R1 ===> R3) (f1 o g1) (f2 o g2)
\end{tabbing}}
The operator {\tt o} has type
{\tt ('b ->\;'c) -> ('a ->\;'b) -> ('a ->\;'c)},
which is polymorphic and also higher order.
It has three type variables, {\tt 'a}, {\tt 'b}, and {\tt 'c}, so $n = 3$.
It has two arguments, so $k = 2$.
The first argument type is
%$\gamma_1$ =
{\tt 'b -> 'c},
for which
the \quotient{} relation
%for $\gamma_1$
is {\tt R2 ===> R3}.
The second argument type is
%$\gamma_2$ =
{\tt 'a -> 'b},
for which
the \quotient{} relation
%for $\gamma_2$
is {\tt R1 ===> R2}.
The result type is
%$\gamma_c$ =
{\tt 'a -> 'c},
for which
the \quotient{} relation
%for $\gamma_c$
is {\tt R1 ===> R3}.
%The lifted versions of these types are
%$\delta_1$ = {\tt 'e -> 'f},
%$\delta_1$ = {\tt 'd -> 'e},
%$\delta_c$ = {\tt 'd -> 'f}.

Whenever there are arguments to the constant, there are
multiple equivalent ways to state the respectfulness theorem.
For example, the respectfulness theorem for {\tt o} may be given
equally well with any of the following as the main part, after the
{\tt QUOTIENT} conditions:
\pagebreak[2]
{\tt \begin{tabbing}
... $\forall$f\=1 f2 g1 g2 x1 x2. \\
\>    (R2\=\ ===> R3) f1 f2 $\wedge$ (R1 ===> R2) g1 g2 $\wedge$ R1 x1 x2 $\Rightarrow$ \\
\>\>     R3 ((f1 o g1) x1) ((f2 o g2) x2) \\
... $\forall$f1 f2 g1 g2. (R2 ===> R3) f1 f2 $\wedge$ (R1 ===> R2) g1 g2 $\Rightarrow$ \\
\>\>     (R1 ===> R3) (f1 o g1) (f2 o g2) \\
... $\forall$f1 f2. (R2 ===> R3) f1 f2 $\Rightarrow$ \\
\>\>     ((R1 ===> R2) ===> (R1 ===> R3)) (\$o f1) (\$o f2) \\
... ((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) \$o \$o
\end{tabbing}}
The last version has higher order and lesser arity than the
earlier versions.  In fact, the four versions above have arities
3, 2, 1, and 0, respectively.
Interestingly, the last version contains no variables (outside of the
relation variables).
The earlier versions may be easier to understand and prove than the
last version.  For the quotient package's internal use, all respectfulness
theorems are automatically converted to the highest order and lowest
arity possible, usually with arity zero.

A substantial collection of these respectfulness theorems for various
standard polymorphic functions of the HOL logic have been proven already and
is available in the quotient library theories (see Table 1).
If there is a need to use a
polymorphic function not covered by these, the corresponding respectfulness
theorem can be proven by the user, using the same approach as for the example
theorems above, as shown in the theory scripts of the quotient library.


%
\subsection{Theorems to be lifted: {\tt old\_thms}}
%
\label{oldtheorem}

%\item
{\tt old\_thms} are the theorems to be lifted.  They should involve only
constants (including functions) of the lower, original level,
with no mention of any lifted constants or functions.
The constants involved must respect
the equivalence relations involved,
as justified by theorems included
in {\tt respects} (see section \ref{respectfulness})
and {\tt poly\_respects} (see section \ref{polyrespects}).
The constants must also be either constants being lifted, or else constants
preserved by the quotient, as justified by theorems included in
{\tt poly\_preserves} (see section \ref{polypreserves}).
Each theorem must not have any free variables, and it also must not
have any hypotheses, only a conclusion.



%
\section{Restrictions on lifting of theorems}
%
\label{restrictions}

This section describes the restrictions needed for theorems to lift;
the next section relaxes these somewhat, but
properly, theorems should obey these restrictions.

It is important to remember that even if all the necessary information
is provided properly, not all theorems of the lower level
can be successfully lifted.

To successfully lift, all of the functions a theorem mentions must
respect the equivalence relations involved in creating the lifted types.
While for the most part properties that are intended to be true at
both levels will be expressed in theorems that will lift, there are
significant issues that can arise.

The first issue is that the normal equality relation ($=$) between elements
of a lower type is a function that does not respect the equivalence
relation for that type.  This means that theorems that mention the
equality of elements of the lower type will not in general lift.
Usually the statement of the theorem should be revised,
with the equivalence relation substituted for the equality relation;
this is a different theorem which will in general require its own proof.
Then if the lifting is successful, it will lift to
a higher version where the equivalence between lower values has been
replaced by equality between higher values.
%This is entirely consistent with the meaning of the lifting operation.

The second issue is that the universal and existential quantification
operators
%({\tt !}, {\tt ?}, or $\forall$, $\exists$)
are not in general respectful.
%This has a significant impact, since these operators are so universally used.
In particular, quantification over function types
may consider functions that are not respectful.
For example, in the lambda calculus example, one theorem to be
lifted is the induction theorem:
{\tt \begin{tabbing}
\hspace{5.5mm}
    $\vdash \forall$P\=. \\
\>       ($\forall$v. P (Var1 v)) $\wedge$ \\
\>       ($\forall$t t0. P t $\wedge$ P t0 $\Rightarrow$ P (App1 t t0)) $\wedge$ \\
\>       ($\forall$t. P t $\Rightarrow$ $\forall$v. P (Lam1 v t)) $\Rightarrow$ \\
\>       ($\forall$t. P t)
\end{tabbing}}

In this theorem the variable {\tt P} has type {\tt term1 -> bool}.
This variable is universally quantified, so all possible functions of
this type are considered as possible values of {\tt P}.
Unfortunately, some functions of this type do not respect the
alpha-equivalence of terms.  This respectfulness would be expressed as
\begin{center}
{\tt $\forall$t1 t2. ALPHA t1 t2 $\Rightarrow$ (P t1 = P t2)}
\end{center}
But this is not true of all functions
of the type {\tt term1 -> bool}.
For example, consider the particular function {\tt P1} defined by
structural recursion as
{\tt \begin{tabbing}
\hspace{22.0mm}
       \=($\forall$x. \ \ P1 (Var1 x) \ \ = F) $\wedge$ \\
\>     ($\forall$t u. P1 (App1 t u) = P1 t $\vee$ P1 u) $\wedge$ \\
\>     ($\forall$x u. P1 (Lam1 x u) = P1 u $\vee$ (x = "a"))
\end{tabbing}}
Then {\tt P1 t} is true if and only if the term {\tt t} contains
a subexpression of the form {\tt Lam1 "a" u}, where the bound variable
is {\tt "a"}.  This {\tt P1} does not satisfy the respectfulness principle
since, for example, {\tt ALPHA (Lam1 "a" (Var1 "a")) (Lam1 "b" (Var1 "b"))}
but then {\tt P1 (Lam1 "a" (Var1 "a"))} is true while
{\tt P1~(Lam1 "b" (Var1 "b"))} is false.

The point is that if such non-respectful functions are considered as
possible values of {\tt P}, then it becomes impossible to lift the
theorem, and in fact in general it would be unsound to do so.
The higher version of the theorem will describe quantification over
functions of the higher types, and these functions correspond only to
respectful functions of the lower types.  Non-respectful functions at the
lower level have
{\bf no} corresponding function at the higher level.  So the statement of the
theorem needs to be revised to quantify only over functions which are
respectful.
For the example above, the theorem needs to be
rephrased
%and reproven
as
{\tt \begin{tabbing}
$\vdash \forall$P\=\ :: respects (ALPHA ===> \$=). \\
\>     ($\forall$v. P (Var1 v)) $\wedge$ \\
\>     ($\forall$t t0 :: respects ALPHA. P t $\wedge$ P t0 $\Rightarrow$ P (App1 t t0)) $\wedge$ \\
\>     ($\forall$t :: respects ALPHA. P t $\Rightarrow$ $\forall$v. P (Lam1 v t)) $\Rightarrow$ \\
\>     ($\forall$t :: respects ALPHA. P t)
\end{tabbing}}

This notation uses the restricted quantifier notation
{\tt $\forall${\it x} :: {\it restriction}. {\it body}},
%which is
the same as
{\tt RES\_FORALL {\it restriction} ($\lambda$x. {\it body})},
introduced in
the {\tt res\_quan} library. It also uses the {\tt respects} operator,
defined in {\tt quotientTheory} as
\begin{center}
{\tt respects R (x:'a) = R x x}
\end{center}
The rephrased induction theorem
states that the variable {\tt P}
is universally quantified over all functions of type {\tt term1 -> bool}
such that those functions respect alpha-equivalence on their domain
{\tt term1}
(and equality on their range,
{\tt bool}),
i.e., {\tt respects (ALPHA ===> \$=) P}, which is equal to
$$\forall t,t_0 : {\tt term1}.\
{\tt ALPHA}\ t\ t_0 \Rightarrow ({\tt P}\ t = {\tt P}\ t_0).$$
Then the revised version of the induction theorem can be successfully
lifted.

In general, the {\tt $\forall$} and {\tt $\exists$}
operators should be replaced by the
{\tt RES\_FORALL} and
{\tt RES\_EXISTS} operators,
with {\tt respects R} as the restriction, where {\tt R} is the
\quotient{} relation for the type being quantified over.
This replacement applies even if {\tt R} is simply an equivalence relation,
where of course {\tt R x x} always holds by reflexivity, and so
no elements of the quantification are excluded.
However, when {\tt R} is simple equality, as for types not being lifted,
no replacement of {\tt $\forall$} or {\tt $\exists$}
is necessary.
{\tt RES\_FORALL} and {\tt RES\_EXISTS} can be
expressed more conveniently using the
``{\tt $\forall$\_::\_.\_}'' and
``{\tt $\exists$\_::\_.\_}''
restriction notation, as shown above.
%but unfortunately {\tt RES\_EXISTS\_EQUIV} cannot.

Finally, on occasion we wish to lift
a theorem to create a higher version that contains
a unique existance quantifier ($\exists$!).
Such a theorem
states that for one and only one instance of the quantified variable,
a property holds.  But that single element at the higher level corresponds
to an entire equivalence class of elements at the lower level.
To lift some lower theorem to such a statement,
the lower theorem must state that the property holds just and only
for elements of that equivalence class, rather than for some single element.
Therefore one cannot simply lift from
a lower version of $\exists$! to a higher version of $\exists$!.  Instead, we
must introduce a new operator, {\tt RES\_EXISTS\_EQUIV} of type
{\tt ('a -> 'a -> bool) -> ('a -> bool) -> bool}.
{\tt \begin{tabbing}
\hspace{20mm}
         RES\=\_EXISTS\_EQUIV R P = \\
\>          ($\exists$x::respects R. P x) $\wedge$ \\
\>          ($\forall$x y::respects R. P x $\wedge$ P y $\Rightarrow$ R x y)
\end{tabbing}}
The first argument {\tt R} is the \quotient{} relation for
the type being quantified over,
and the second argument {\tt P} is the predicate
which is being stated as true for some element of that type
which respects {\tt R}.
%The meaning of
{\tt RES\_EXISTS\_EQUIV R P} means that there exist
some elements which are respectful of {\tt R} and which satisfy {\tt P},
%and all elements which are respectful of {\tt R} and which satisfy {\tt P}
and all such elements
are equivalent according to {\tt R}.

For convenience, {\tt RES\_EXISTS\_EQUIV} can also be represented using a
new restricted quantification binder, $\exists$!!.  The parser will translate
{\tt $\exists !!$x::R. P x} into {\tt RES\_EXISTS\_EQUIV R ($\lambda$x. P x)},
and the prettyprinter will reverse this.
In order to use this notation, in each HOL session
one must first execute
\begin{verbatim}
val _ = associate_restriction ("?!!", "RES_EXISTS_EQUIV");
\end{verbatim}

When attempting to lift a theorem,
all instances of quantifying by $\exists$! over types being lifted
should be replaced by instances of $\exists$!! ({\tt RES\_EXISTS\_EQUIV})
along with the appropriate \quotient{} relation.
%and the revised theorem proven before attempting lifting to the higher level.
Instances of quantifying by $\exists$! over types not being lifted need
not be modified at all.
Note that where the restricted quantifier versions of $\forall$ and $\exists$
use restrictions of the form {\tt respects~R}, the restricted quantifier
version of $\exists$!! uses just {\tt R} as the restriction.

For example, this arises naturally in
the function existence theorem proposed by Gordon and
Melham for the lambda calculus
\cite{GoMe96}:
\pagebreak[2]
{\tt \begin{tabbing}
\hspace{2.5mm}
   $\vdash \forall$v\=ar app abs. \\
\>      $\exists !$\=hom. \\
\>\>      ($\forall$x. hom (Var x) = var x) $\wedge$ \\
\>\>      ($\forall$t u. hom (App t u) = app (hom t) (hom u)) $\wedge$ \\
\>\>      ($\forall$x u. hom (Lam x u) = abs ($\lambda$y. hom (u <[ [(x,Var y)])))
\end{tabbing}}

\noindent
To create the above theorem, we need to prove
the proper lower version
%at the lower level
{\tt \begin{tabbing}
\hspace{2.5mm}
  $\vdash \forall$v\=ar app abs. \\
\>     $\exists !!$\=hom :: (ALPHA ===> \$=). \\
\>\>     ($\forall$x. hom (Var1 x) = var x) $\wedge$ \\
\>\>     ($\forall$t\=\ u :: respects ALPHA. \\
\>\>\>      hom (App1 t u) = app (hom t) (hom u)) $\wedge$ \\
\>\>     ($\forall$x (u :: respects ALPHA). \\
\>\>\>      hom (Lam1 x u) = abs ($\lambda$y. hom (u <[ [(x,Var1 y)])))
\end{tabbing}}
\noindent
which will then lift.


\begin{comment}

Only those properties which respect
the equivalence relations of the quotient operations will properly lift.
An property which would not lift would be one which
depended on specific information as to which element of an equivalence
class was being referred to.
Some theorems describe
properties which have no direct corresponding theorem at the abstract,
lifted level.  Other theorems may have such a corresponding theorem,
but they may not be strong enough to infer the lifted theorem.

For example, consider the quotient of the non-negative integers
by the equivalence
relation $\sim$ where $n \sim m$ if and only if $n$ and $m$ are either both
even or both odd.  This creates two equivalence classes, which are the
set of even integers and the set of odd integers.  This specifies a new,
lifted type with two values for which we can define the constants,
{\tt EVEN} as the lifted version of {\tt 0} and {\tt ODD}
as the lifted version of {\tt 1}.

At the lower level, we can prove the theorem {\tt $\vdash$ \verb+~+(3 = 5)}.
But this theorem does not lift to the abstract level, where it would be
{\tt $\vdash$ \verb+~+(ODD = ODD)}, which is obviously false.
So not every theorem should or will lift!

At the lower level, we can prove the theorem {\tt $\vdash$ \verb+~+(0 = 1)}.
For this theorem, there {\it is\/}
a corresponding theorem at the abstract level,
{\tt $\vdash$ \verb+~+(EVEN = ODD)}, which should be true.  However, there is just not
enough information in the lower theorem {\tt $\vdash$ \verb+~+(0 = 1)}
to prove the lifted version, because the lower theorem
only states an inequality.  What is actually needed is
{\tt $\vdash$ \verb+~+(0 $\sim$ 1)}, which states that the two values are
not equivalent, which is stronger.
{\tt $\vdash$ \verb+~+(0 $\sim$ 1)} implies that
{\tt $\vdash$ \verb+~+(0 = 1)},
but not the reverse.
{\tt $\vdash$ \verb+~+(0 $\sim$ 1)} is provable at the lower level,
and it will successfully lift to {\tt $\vdash$ \verb+~+(EVEN = ODD)}.

In general, a property which will lift may be composed only of
functions which respect the equivalence relations involved.
This includes ordinary equality!
But an essential problem here is that the equality operation
does not respect the equivalence relation, that is,
$$a_1 \sim a_2 \ \wedge \ b_1 \sim b_2 \ \not\Rightarrow \
 (a_1 = b_1 \ \Leftrightarrow \ a_2 = b_2).$$
An instance of this would be that $3 \sim 3$ and $3 \sim 5$, but then
$3 = 3$ is true while $3 = 5$ is false.

Generally, any mention of equality between elements of a type being
lifted will make a theorem not liftable.  A variant of the theorem
should be proven which substitutes equivalence for the equality.
%
This should really not be surprising, since the purpose of collapsing
equivalence classes into single entities is meant to render the results
indistinguishable.  Therefore properties which rely on those distinctions
will not translate to the higher level, which in particular excludes
the equality relation between values which are now being declared as
equivalent.

\end{comment}

%\end{enumerate}

%
\section{Support for non-standard lifting}
%
\label{nonstandard}

The {\tt define\_quotient\_types} tool
for lifting theorems is actually less
demanding and more forgiving than has been described up to this point.
Automation has been added to recognize several common
situations of theorems which may not be in the proper form, but are
strong enough to imply the proper form.  These are quietly converted
and then lifted.

Despite the objections to the use of equality
in theorems to be lifted mentioned above, in practice equality is commonly used.
Many theorems to be lifted have the form
{\tt $\vdash$ a = b}, for some expressions {\tt a} and {\tt b} whose type is
being lifted.
In fact,
if $\sim$ is an equivalence relation,
this equality implies {\tt $\vdash$ a $\sim$ b}.
The tool recognizes this common case and automatically proves
the needed revised
theorem that only mentions equivalence instead of equality.
This can then be lifted.

Similarly, theorems of the form {\tt $\vdash$ P $\Rightarrow$ (a = b)}, or even more
general examples, can also be
automatically revised and then lifted.

Universal or existential restricted quantification, where the
restriction is of the form {\tt respects R}, for {\tt R} an equivalence
relation, do not actually restrict any elements from the quantification.
Thus these are really equal to the original ordinary quantification,
and the tool is able to create and prove the version with such
restricted quantifications from a user-supplied theorem with normal
quantification in those places.

In addition, theorems which are universal quantifications
%with that quantification
at the outer level of the theorem, may
imply the restricted universal quantifications (their proper form)
%using restricted quantification
over respectful values.
The proper form is automatically proven and then lifted.
For example, the tool can lift the
lambda calculus induction theorem given earlier without the user first
converting it to proper form.

Finally, theorems which involve unique existance
quantification $\exists$! restricted over functions which are respectful,
may imply the corresponding theorem using the
restricted $\exists$!!
%{\tt RES\_EXISTS\_EQUIV}
operator.  For example, in the lambda
calculus example, we have proven
%it is possible to prove
at the lower level
{\tt \begin{tabbing}
 $\vdash \forall$v\=ar app abs. \\
\>    $\exists !$\=hom :: respects (ALPHA ===> \$=). \\
\>\>    ($\forall$x. hom (Var1 x) = var x) $\wedge$ \\
\>\>    ($\forall$t u. hom (App1 t u) = app (hom t) (hom u)) $\wedge$ \\
\>\>    ($\forall$x u. hom (Lam1 x u) = abs ($\lambda$y. hom (u <[ [(x,Var1 y)])))
\end{tabbing}}

\noindent
The tool will first automatically prove the proper version:
{\tt \begin{tabbing}
 $\vdash \forall$v\=ar app abs. \\
\>    $\exists !!$\=hom :: ALPHA ===> \$=. \\
\>\>    ($\forall$x. hom (Var1 x) = var x) $\wedge$ \\
\>\>    ($\forall$t\=\ u :: respects ALPHA. \\
\>\>\>     hom (App1 t u) = app (hom t) (hom u)) $\wedge$ \\
\>\>    ($\forall$x (u :: respects ALPHA). \\
\>\>\>     hom (Lam1 x u) = abs ($\lambda$y. hom (u <[ [(x,Var1 y)])))
\end{tabbing}}

\noindent
and then lift the proper version to the desired higher version of this theorem:
{\tt \begin{tabbing}
 $\vdash \forall$v\=ar app abs. \\
\>    $\exists !$\=hom. \\
\>\>    ($\forall$x. hom (Var x) = var x) $\wedge$ \\
\>\>    ($\forall$t u. hom (App t u) = app (hom t) (hom u)) $\wedge$ \\
\>\>    ($\forall$x u. hom (Lam x u) = abs ($\lambda$y. hom (u <[ [(x,Var y)])))
\end{tabbing}}

In general, of course, this revising may not work.
If the tool cannot automatically prove the proper version from the theorem
it is given, it will print out an error message showing the needed revised
proper form.  The user should prove the proper version manually
and then submit
it
%the proper theorem
to the tool for lifting.

Finally, we would like to describe some possible reasons to consider
when theorems do not lift, apart from improper form as above.  First,
every constant mentioned in the theorem that takes or returns values
of types being lifted must be described in a respectfulness theorem,
whether in the {\tt respects} or {\tt poly\_respects} arguments.
Also, every such constant in the theorem
must be either one being lifted to a new constant in the {\tt defs} argument,
or described in a preservation theorem in the {\tt poly\_preserves} argument.
Every partial equivalence relation mentioned in any of these theorems
should be either one of those mentioned in the {\tt types} argument,
or an extension of these,
using the relation operators mentioned in sections
\ref{equivalence} and
\ref{quotientrelation}.
If the type of any constant in any theorem
involves type operators, like lists or functions, then the associated
quotient extension theorems must be provided in the
{\tt tyop\_quotients} argument.
%except for {\tt FUN\_QUOTIENT}, which is builtin by default.
Likewise, the equivalence extension theorems (if available),
and the associated relation and map function simplification theorems
should be provided
in the {\tt tyop\_equivs} and {\tt tyop\_simps} arguments.
The error message associated with the exception thrown may help localize
the error.
The process of the quotient operation may be observed in more detail
by setting the variable {\tt quotient.chatting := true}.
Lastly, during development it may be more convenient to use the
{\tt define\_quotient\_types\_rule} tool, so that the {\tt LIFT\_RULE}
function it returns may be applied to candidate lower theorems individually
and repeatedly.  This helps to retry lifting a troublesome theorem
in isolation until it successfully lifts.


%
\section{Lifting Sets}
%
\label{liftingsets}

The facilities provided so far for higher order quotients are flexible
and extensible for the addition of support for new type operators, with
their own associated quotient extension theorems, simplification theorems,
perhaps equivalence extension theorems, and respectfulness and
preservation theorems for the
constants associated with the type operator.

One commonly used type is sets, which are implemented in the Higher
Order Logic theorem prover through the library {\tt pred\_set}.  No actual
new type is used here, but sets are represented by the function type
{\tt 'a -> bool}, where {\tt 'a} is the underlying type of the elements
of the set.
In fact, there is a close identity between a set and its characteristic
function.  Nevertheless, it is helpful and intuitive at times to think
of sets as sets, not functions, and many normal set operators, such
as {\tt INSERT}, {\tt SUBSET}, and {\tt UNION}, are provided.

For this type of sets,
if the partial equivalence relation
on the underlying type is $R$, then
the extension of $R$
to the set type is
$R \ \mbox{\tt ===>} \ (\mbox{\tt \$=:bool->bool->bool})$.
Essentially, sets behave as a specialization of the
function quotient extension theorem, where the domain is the base type of $R$
and the range is {\tt bool}, as in
{\tt \begin{tabbing}
SET\=\_QUOTIENT: \\
\>  $\vdash$  \=$\forall R\;$\=${\it abs}\;{\it rep}.\
          \langle R,{\it abs},{\it rep} \rangle \Rightarrow
          \langle R\;\mbox{\tt ===>}\;\mbox{\tt \$=},\
            {\it rep}\;\mbox{\tt -->}\;{\tt I},\
            {\it abs}\;\mbox{\tt -->}\;{\tt I}
          \rangle$
\end{tabbing}}
The associated abstraction function
is ${\it rep}\;\mbox{\tt -->}\;{\tt I}$,
and the associated representation function
is ${\it abs}\;\mbox{\tt -->}\;{\tt I}$.
Note that the use of $abs$ vs. $rep$ is counterintuitive.

When lifting theorems that contain instances of polymorphic set operators
applied to values of types being lifted, some of the normal set
operators are preserved across the quotient operation, but several are
not.  For these operators, we have provided new, similar operators
which take into account the partial equivalence relation(s) involved,
and thus do successfully lift to their normal set operator counterpart.

For example, for the set operator {\tt DIFF}, no problems arise, and
we can prove its respectfulness and preservation theorems of the normal
form.

{\tt \begin{tabbing}
DIFF\_PRS: \\
\hspace{5.5mm}
    $\vdash$ \=$\forall$R \=(abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\
\>\>     $\forall$s t. \=s DIFF t = \\
\>\>\>     (rep --> I) (((abs --> I) s) DIFF ((abs --> I) t)) \\
\\
DIFF\_RSP: \\
\hspace{5.5mm}
    $\vdash$ $\forall$R (abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\
\>\>     $\forall$s1 s2 t1 t2. \\
\>\>\>     (R ===> \$=) s1 s2 $\wedge$ (R ===> \$=) t1 t2 $\Rightarrow$ \\
\>\>\>     (R ===> \$=) (s1 DIFF t1) (s2 DIFF t2)
\end{tabbing}}

But  the following operators are {\it not\/} preserved, and have the indicated
associated ``regular'' versions:

\begin{center}
{\tt \begin{tabular}{|c|c|}
\hline
{\rm Normal} & {\rm Regular} \\
\hline
INSERT   & INSERTR \\
DELETE   & DELETER  \\
SUBSET   & SUBSETR \\
PSUBSET  & PSUBSETR \\
\ DISJOINT \ & \ DISJOINTR \  \\
FINITE   & FINITER  \\
GSPEC    & GSPECR  \\
IMAGE    & IMAGER  \\
\hline
\end{tabular}}
\end{center}

Even if the original operator is infix, all of the new operators
are prefix operators, to ease the addition of the new arguments.

Most of these regular operators take one new argument, which is the
partial equivalence relation of the underlying type of the set.
For {\tt GSPECR} and {\tt IMAGER}, there are two new arguments,
which are the partial equivalence relations of
the types used for the polymorphic type variables of the original
{\tt GSPEC} or {\tt IMAGE}.  To make this clearer, here are the
preservation theorems for these two operators.

{\tt \begin{tabbing}
GSPEC\_PRS: \\
\hspace{1.5mm}
    $\vdash$ \=$\forall$R\=1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\
\>           $\forall$R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\
\>\>     $\forall$f. \=GSPEC f = \\
\>\>\>     (rep2 --> I) (GSPECR R1 R2 ((abs1 --> (rep2 \#\# I)) f)) \\
\\
IMAGE\_PRS: \\
\hspace{1.5mm}
    $\vdash$ $\forall$R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\
\>           $\forall$R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\
\>\>     $\forall$f s. IMAGE f s = \\
\>\>\>     (rep2 --> I) (IMAGER R1 R2 \=((abs1 --> rep2) f) \\
\>\>\>\>                                ((abs1 --> I) s))
\end{tabbing}}

The polymorphic preservation and respectfulness theorems for all these
operators are found in {\tt quotient\_pred\_setTheory}, where e.g. the
names of these theorems for the {\tt INSERT} operator are
{\tt INSERT\_PRS} and {\tt INSERTR\_RSP}, respectively.

To ease the process of formulating the appropriate regular version of a
theorem that a user wishes to lift, the tools will examine a given
theorem to see if it is regular, and if not, will construct a regular
version which if proved by the user will (hopefully) lift.
Here are some examples.

{\tt \begin{tabbing}
val \=LIFT\_RULE =  \\
\>  define\_quotient\_types\_full\_rule  \\
\>  \{types = [\{name = "term", equiv = ALPHA\_EQUIV\}],  \\
\>  \ defs = fnlist,  \\
\>  \ tyop\_equivs = [],  \\
\>  \ tyop\_quotients = [],  \\
\>  \ tyop\_simps = [],  \\
\>  \ respects = respects,  \\
\>  \ poly\_preserves = [\=IN\_PRS,EMPTY\_PRS,UNIV\_PRS,UNION\_PRS,  \\
\>\>                   INTER\_PRS,SUBSET\_PRS,PSUBSET\_PRS,  \\
\>\>                   DELETE\_PRS,INSERT\_PRS,DIFF\_PRS,GSPEC\_PRS,  \\
\>\>                   DISJOINT\_PRS,FINITE\_PRS,IMAGE\_PRS],  \\
\>  \ poly\_respects \ = [IN\_RSP,EMPTY\_RSP,UNIV\_RSP,UNION\_RSP,  \\
\>\>                   INTER\_RSP,SUBSETR\_RSP,PSUBSETR\_RSP,  \\
\>\>                   DELETER\_RSP,INSERTR\_RSP,DIFF\_RSP,GSPECR\_RSP,  \\
\>\>                   DISJOINTR\_RSP,FINITER\_RSP,IMAGER\_RSP],  \\
  \\
- LIFT\_RULE (INST\_TYPE [alpha |-> ``:'a term1``] EXTENSION)  \\
\ \ handle e => Raise e;  \\
  \\
Exception raised at quotient.REGULARIZE:  \\
Could not lift the irregular theorem  \\
$\vdash$ $\forall$s t. (s = t) $\Leftrightarrow$ $\forall$x. x IN s $\Leftrightarrow$ x IN t  \\
May try proving and then lifting  \\
$\forall$s t::respects (ALPHA ===> \$=).  \\
\ \ (ALPHA ===> \$=) s t $\Leftrightarrow$ $\forall$x::respects ALPHA. x IN s $\Leftrightarrow$ x IN t  \\
! Uncaught exception:   \\
! HOL\_ERR  \\
  \\
- LIFT\_RULE (INST\_TYPE [alpha |-> ``:'a term1``] SUBSET\_TRANS)  \\
\ \ handle e => Raise e;  \\
  \\
Exception raised at quotient.REGULARIZE:  \\
Could not lift the irregular theorem  \\
$\vdash$ $\forall$s t u. s SUBSET t $\wedge$ t SUBSET u $\Rightarrow$ s SUBSET u  \\
May try proving and then lifting  \\
$\forall$s t u::respects (ALPHA ===> \$=).  \\
\ \ SUBSETR ALPHA s t $\wedge$ SUBSETR ALPHA t u $\Rightarrow$ SUBSETR ALPHA s u  \\
! Uncaught exception:   \\
! HOL\_ERR  \\
  \\
- LIFT\_RULE  \\
\ \ \ \ (INST\_TYPE [alpha |-> ``:'a term1``, beta |-> ``:'b term1``]  \\
\ \ \ \ \ \        INJECTIVE\_IMAGE\_FINITE);  \\
  \\
Exception raised at quotient.REGULARIZE:  \\
Could not lift the irregular theorem  \\
$\vdash$ $\forall$f.
        ($\forall$x y. (f x = f y) $\Leftrightarrow$ (x = y)) $\Rightarrow$  \\
\ \ \ \ \ \ $\forall$s. FINITE (IMAGE f s) $\Leftrightarrow$ FINITE s  \\
May try proving and then lifting  \\
$\forall$f::respects (ALPHA ===> ALPHA).  \\
\ \ ($\forall$x y::respects ALPHA. ALPHA (f x) (f y) $\Leftrightarrow$ ALPHA x y) $\Rightarrow$  \\
\ \ \ $\forall$s::respects (ALPHA ===> \$=).  \\
\ \ \ \ \ FINITER ALPHA (IMAGER ALPHA ALPHA f s) $\Leftrightarrow$ FINITER ALPHA s  \\
! Uncaught exception:   \\
! HOL\_ERR
\end{tabbing}}

In each case the suggested regular version of the theorem can be
copied from the error message,
proven by hand, and then submitted to the tool for lifting.

Here are the names of the preservation and respectfulness theorems
for polymorphic set operators provided in the quotient library.

\begin{table}
\begin{center}
{\bfseries TABLE 2.\\
Preservation
%Definition
and Respectfulness Theorems for Polymorphic Set Operators}\\[1ex]
\begin{tabular}{|lll|l|l|}
\hline
\multicolumn{3}{|l|}
{Lifted Operators} &
%Lifted
Preservation
%Definition
Theorems & Respectfulness Theorems \\
\hline
{\tt IN} & & & {\tt IN\_PRS} & {\tt IN\_RSP} \\
{\tt EMPTY} & & & {\tt EMPTY\_PRS} & {\tt EMPTY\_RSP} \\
{\tt UNIV} & & & {\tt UNIV\_PRS} & {\tt UNIV\_RSP} \\
{\tt INTER} & & & {\tt INTER\_PRS} & {\tt INTER\_RSP} \\
{\tt UNION} & & & {\tt UNION\_PRS} & {\tt UNION\_RSP} \\
{\tt DIFF} & & & {\tt DIFF\_PRS} & {\tt DIFF\_RSP} \\
{\tt INSERTR} & $\rightarrow$ & {\tt INSERT}
& {\tt INSERT\_PRS} & {\tt INSERTR\_RSP} \\
{\tt DELETER} & $\rightarrow$ & {\tt DELETE}
& {\tt DELETE\_PRS} & {\tt DELETER\_RSP} \\
{\tt DISJOINTR} & $\rightarrow$ & {\tt DISJOINT}
& {\tt DISJOINT\_PRS} & {\tt DISJOINTR\_RSP} \\
{\tt GSPECR} & $\rightarrow$ & {\tt GSPEC}
& {\tt GSPEC\_PRS} & {\tt GSPECR\_RSP} \\
{\tt SUBSETR} & $\rightarrow$ & {\tt SUBSET}
& {\tt SUBSET\_PRS} & {\tt SUBSETR\_RSP} \\
{\tt PSUBSETR} & $\rightarrow$ & {\tt PSUBSET}
& {\tt PSUBSET\_PRS} & {\tt PSUBSETR\_RSP} \\
{\tt FINITER} & $\rightarrow$ & {\tt FINITE}
& {\tt FINITE\_PRS} & {\tt FINITER\_RSP} \\
{\tt IMAGER} & $\rightarrow$ & {\tt IMAGE}
& {\tt IMAGE\_PRS} & {\tt IMAGER\_RSP} \\
\hline
\end{tabular}
\\
\end{center}
An arrow
({\it lower} $\rightarrow$ {\it higher})
indicates that in
preservation theorems,
%definition,
the lower operator
is different
%differs
from the higher,
%otherwise
else
it
%the operator
is the same.
%\\
Respectfulness theorems concern
{\it lower}.
%the lower operator.
\end{table}

In addition, several related theorems are provided, including the
definitions of the new operators and some of their interactions with other
set operators.

\pagebreak[4]
{\tt \begin{tabbing}
IN\_INSERTR: \\
\hspace{5.5mm}
\=$\vdash$ $\forall$R\= x s y. y IN INSERTR R x s $\Leftrightarrow$ R y x $\vee$ y IN s  \\
IN\_DELETER: \\
\>$\vdash$ $\forall$R s x y. y IN DELETER R s x $\Leftrightarrow$ y IN s $\wedge$ \verb+~+R x y  \\
IN\_GSPECR: \\
\>$\vdash$ $\forall$R1 R2 f v.  \\
\>\> v IN GSPECR R1 R2 f $\Leftrightarrow$  \\
\>\> $\exists$x::respects R1. (R2 \#\#\# \$=) (v,T) (f x)  \\
IN\_IMAGER:  \\
\>$\vdash$ $\forall$R1 R2 y f s.  \\
\>\>     y IN IMAGER R1 R2 f s $\Leftrightarrow$  \\
\>\>     $\exists$x::respects R1. R2 y (f x) $\wedge$ x IN s
%FINITER\_def: \\
%\>    $\vdash$ $\forall$R s.
%         FINITER R s $\Leftrightarrow$  \\
%\>\>     !P\=::respects ((R ===> \$=) ===> \$=).  \\
%\>\>\>     P \{\} $\wedge$
%           ($\forall$s\=::respects (R ===> \$=).  \\
%\>\>\>\>      P s ==> $\forall$e::respects R. P (INSERTR R e s)) $\Rightarrow$  \\
%\>\>\>     P s
\end{tabbing}}

These facilities for set operators are presented to be helpful,
but they are in
%a state of
development, and should be considered
experimental and subject to change.
%They will probably change somewhat in future versions.

%\vspace{0.7in}


%
\section{The Sigma Calculus}
%
\label{sigmacalculus}

The untyped sigma calculus was introduced by Abadi and Cardelli in
{\it A Theory of Objects} \cite{AbCa96}.
It highlights the concept of objects,
rather than functions.
%including the ideas of messages, methods, arguments to methods,
%and replacing an existing method in an object by another.

We will use the sigma calculus as an example to demonstrate the quotient
package tools.
We will first define an initial or ``pre-''version of the
language syntax,
and then create the refined or ``pure'' version
by performing a quotient operation on the initial version.

The pre-sigma calculus contains terms denoting objects and methods.
We define the sets of object terms $O_1$ and method terms $M_1$ inductively as

(1) $x \in O_1$ for all variables $x$;

(2) $m_1, \ldots,\, m_n \in M_1 \,\Rightarrow\,
     [ l_1 \mathbin{=} m_1,\,\ldots,\,l_n \mathbin{=} m_n ] \in O_1$
     for all labels $l_1,\ldots,\,l_n$;

(3) $a \in O_1 \ \Rightarrow \ a.l \in O_1$ for all labels $l$;

(4) $a \in O_1 \ \wedge \ m \in M_1 \ \Rightarrow \
     a.l \Lleftarrow m \in O_1$ for all labels $l$;

(5) $a \in O_1 \ \Rightarrow \ \varsigma(x)a \in M_1$ for all varibles $x$.

$[ l_1 \mathbin{=} m_1, \,\ldots,\, l_n \mathbin{=} m_n ]$ denotes a
{\it method dictionary,}
as a finite list of {\it entries}, each $l_i \mathbin{=} m_i$
consisting of a label and a method.
There should be no duplicates among the labels, but if there are, the first
one takes precedence.

The form $a.l$ denotes the invocation of the method labelled $l$ in the
object $a$.  The form $a.l \Lleftarrow m$ denotes the update of the object
$a$, where the method labelled $l$ (if any) is replaced by the new
method $m$.  The form $\varsigma(x)a$ denotes a method with one formal
parameter, $x$, and a body $a$.  $\varsigma$ is a binder, like $\lambda$
in the lambda calculus.  $x$ is a bound variable,
and the scope of $x$ is the body $a$.
In this scope, $x$ represents the ``self'' parameter,
%that is,
the object itself which contains this method.
%Thus in the sigma calculus
%there are no other arguments sent with a message other than simply the
%label itself.

Given the pre-sigma calculus, we define the pure sigma
calculus by identifying object and method terms which are alpha-equivalent
\cite{Bar81}.
Thus in the pure sigma calculus, $\varsigma(x)x.l_1 = \varsigma(y)y.l_1$,
$[l_1 \mathbin{=} \varsigma(x)x] = [l_1 \mathbin{=} \varsigma(y)y]$, et cetera.
This is accomplished
by forming the quotients of the types of pre-sigma calculus
object and method terms by their
alpha-equivalence relations.
Thus $O = O_1 / {\equiv}_{\alpha}^o$
and $M = M_1 / {\equiv}_{\alpha}^m$,
where ${\equiv}_{\alpha}^o$ and ${\equiv}_{\alpha}^m$ are the
respective alpha-equivalence relations.

%For more on the syntax and semantics of the sigma calculus, with
%examples, please see
%\cite{AbCa96}.

%As an example of a programming language, it is
%interesting that the sigma calculus is mutually recursive in
%its definition.  This is easily seen by noting that $O_1$ is defined in
%terms of $M_1$, and vice versa.  However, the recursive structure is
%actually more deep than might at first appear.  The list structure
%that is appealed to in the dictionary form is itself a recursively
%defined structure, and this introduces its own complexities, as we
%shall see later.
%It is possible to create a de-Bruin-style representation of the
%sigma calculus which has only one type, as done by Sidi O. Ehmety,
%but for a name-carrying syntax, mutual recursion is natural.
%The mutual recursion inherent in these
%fundamental definitions of the syntax
%has profound implications for all formal studies of this system.

%
\section{The Pre-Sigma Calculus in HOL}
%
\label{presigmacalculus}

HOL supports the definition of new nested mutually recursive types
by the {\tt Hol\_datatype} function in the
{\tt bossLib} library.
%(HOL System Description Manual, section 5.2.1).
%as described in section 5.2.1 of the HOL System Description Manual.

%In addition to defining new types, this tool also defines the
%constructor functions for the various cases of how values of the types
%may be constructed, and proves several theorems about the interrelationships
%of these types and
%%constructor
%functions.
%%This includes the existence of primitive recursive functions on these
%%new types, a structural induction principle, the distinctiveness and
%%one-to-one properties of the constructors, and a cases theorem.

%All of the type definition, constructor function definition, and
%subsequent proofs of the above properties is done completely securely,
%as a definitional extension of the HOL logic.
%This is an
%excellent example of appropriate automation, where a terse but powerful
%description is completely automatically processed to yield effective and
%nontrivial results.

%We illustrate the use of this tool with the example mentioned.
The syntax
of the pre-sigma calculus
is defined as follows.

\begin{verbatim}
val _ = Hol_datatype

       (* obj1 ::= x | [li=mi] i in 1..n |  a.l | a.l:=m *)
        ` obj1 = OVAR1 of var
               | OBJ1 of (string # method1) list
               | INVOKE1 of obj1 => string
               | UPDATE1 of obj1 => string => method1 ;

       (* method1 ::= sigma(x)a *)
          method1 = SIGMA1 of var => obj1 ` ;
\end{verbatim}

\noindent
This creates the new mutually recursive types {\tt obj1} and {\tt method1},
and also the constructor functions

\begin{center}
\begin{tabular}[t]{l@{\hspace{0.5cm}}c@{\hspace{0.5cm}}l}
{\tt OVAR1} & {\tt :} & {\tt var -> obj1} \\
{\tt OBJ1} & {\tt :} & {\tt (string \# method1) list -> obj1} \\
{\tt INVOKE1} & {\tt :} & {\tt obj1 -> string -> obj1} \\
{\tt UPDATE1} & {\tt :} & {\tt obj1 -> string -> method1 -> obj1} \\
{\tt SIGMA1} & {\tt :} & {\tt var -> obj1 -> method1} \\
\end{tabular}
\end{center}

It also creates associated theorems for induction, function existance,
and one-to-one and distinctiveness properties of the constructors.

The definition above goes beyond
%is more sophisticated than
simple mutual recursion
of types, to involve what is called ``nested recursion,'' where a type
being defined may appear deeply nested under type operators such as
{\tt list}, {\tt prod}, or {\tt sum}.  In the above definition,
in the line defining
the {\tt OBJ1} constructor function, the type {\tt method1} is nested,
first as the right part of a pair type, and then as the element type of
a list type.

The {\tt Hol\_definition} tool automatically compensates for this
complexity, creating in effect {\bf \it four\/} new types, not simply two.
It is as if the tool created the intermediate types

\begin{center}
\begin{tabular}[t]{l@{\hspace{0.5cm}}c@{\hspace{0.5cm}}l}
{\tt entry1} & {\tt =} & {\tt string \# method1} \\
{\tt dict1}  & {\tt =} & {\tt (entry1)list}
\end{tabular}
\end{center}

\noindent
except that these types are actually formed by the
{\tt prod}
and
{\tt list}
type operators, not by creating new types.
%Then the {\tt OBJ1} constructor could have been defined
%as {\tt OBJ1 of dict1}.
It turns out that when defining mutually recursive functions on these
types, there must be {\it four} related functions defined simultaneously,
one for each of the types
{\tt obj1}, {\tt dict1}, {\tt entry1}, and {\tt method1}.
Similarly, when proving theorems about these functions,
one must use mutually recursive structural induction,
where the goal has four parts, one for each of the types.

%
%In fact, it is handled somewhat as if the user had typed,
%
%\begin{verbatim}
%val _ = Hol_datatype
%
%       (* obj1 ::= x | d | a.l | a.l:=m *)
%        ` obj1 = OVAR1 of var
%               | OBJ1 of dict1
%               | INVOKE1 of obj1 => string
%               | UPDATE1 of obj1 => string => method1 ;
%
%       (* dict1 ::= [] | e :: d *)
%          dict1 = NIL
%                | CONS of entry1 => dict1 ;
%
%       (* entry ::=  s = m  *)
%          entry1 = MK_PAIR of string => method1 ;
%
%       (* method1 ::= sigma(x)a *)
%          method1 = SIGMA1 of var => obj1 ` ;
%\end{verbatim}
%
%\noindent
%except that the constructor functions {\tt NIL}, {\tt CONS}, and
%{\tt MK\_PAIR} already exist.  Using the nested recursion form, as
%first given,
%means that the types corresponding to {\tt dict1} and
%{\tt entry1} in the second form are actually represented as nested
%combinations of {\tt obj1} and {\tt method1}.
%
%\begin{center}
%\begin{tabular}[t]{l@{\hspace{0.5cm}}l}
%{\tt dict1}  & {\tt = (string \# method1)list} \\
%{\tt entry1} & {\tt = string \# method1}
%\end{tabular}
%\end{center}
%
%For clarity's sake, we will henceforth use the names {\tt dict1} and
%{\tt entry1} as abbreviations for the longer true types given above.
%
%The nested version is advantageous over the larger,
%non-nested version,
%because it means that these types are in fact real lists and pairs,
%and we can use all of the well-developed support in HOL to deal with
%lists and pairs, without having to reinvent the wheel and redo all
%that work for {\tt dict1} and {\tt entry1}.

%The constructors for {\tt obj1} and {\tt method1}
%have the following types.
%
%\begin{center}
%\begin{tabular}[t]{l@{\hspace{0.5cm}}l}
%{\tt OVAR1}   & {\tt : var -> obj1} \\
%{\tt OBJ1}    & {\tt : dict1 -> obj1} \\
%{\tt INVOKE1} & {\tt : obj1 -> string -> obj1} \\
%{\tt UPDATE1} & {\tt : obj1 -> string -> method1 -> obj1} \\
%{\tt SIGMA1}  & {\tt : var -> obj1 -> method1}
%\end{tabular}
%\end{center}
%
%Note that the constructor functions {\tt NIL}, {\tt CONS}, and
%{\tt MK\_PAIR} already apply correctly without modification,
%because they are polymorphic.
%
%\begin{center}
%\begin{tabular}[t]{l@{\hspace{0.5cm}}l}
%{\tt NIL}      & {\tt : dict1} \\
%{\tt CONS}     & {\tt : entry1 -> dict1 -> dict1} \\
%{\tt MK\_PAIR} & {\tt : string -> method1 -> entry1}
%\end{tabular}
%\end{center}

%This mutually recursive type structure has ramifications wherever these
%new types are used.
%In particular, it affects how new mutually recursive functions on
%values of these types are defined, and it affects how theorems about
%the properties of those mutually recursive functions are proven by
%mutually recursive structural induction.

%As mentioned before, there are several theorems proven
%automatically and stored in the current theory.
%These concern such things as an induction principle and
%the distinctiveness and one-to-one properties of constructors.

Now we will construct the pure sigma calculus from the pre-sigma calculus.
%Now, to construct the pure sigma calculus from the pre-sigma calculus,
%we will need to form quotients of these four types by their alpha-equivalence
%relations.


%
\section{The Pure Sigma Calculus in HOL}
%
\label{puresigmacalculus}

We here define the pure sigma calculus in HOL.

Let us assume
that we have defined alpha-equivalence relations for each of the two types
{\tt obj1}
%{\tt dict1}, {\tt entry1},
and {\tt method1}, called
{\tt ALPHA\_obj}
%{\tt ALPHA\_dict}, {\tt ALPHA\_entry},
and {\tt ALPHA\_method},
and that we have proven the
%reflexivity, symmetry, and transitivity of each of these, as theorems called
equivalence theorems for these,
%{\tt ALPHA\_obj\_REFL},
%{\tt ALPHA\_obj\_SYM},
%{\tt ALPHA\_obj\_TRANS}, et cetera.
\begin{center}
\begin{tabular}{l}
{\tt ALPHA\_obj\_EQUIV:} \\
\hspace{0.9cm}
{\tt $\vdash \forall$x y. ALPHA\_obj x y = (ALPHA\_obj x = ALPHA\_obj y)} \\
{\tt ALPHA\_method\_EQUIV:} \\
\hspace{0.9cm}
{\tt $\vdash \forall$x y. ALPHA\_method x y =\;(ALPHA\_method x = ALPHA\_method y)}
\end{tabular}
\end{center}

We specify the constants that are to be lifted:
\begin{verbatim}
- val defs = [{def_name="OVAR_def", fname="OVAR",
               func= (--`OVAR1`--), fixity=NONE},
              {def_name="OBJ_def", fname="OBJ",
               func= (--`OBJ1`--), fixity=NONE},
              {def_name="INVOKE_def", fname="INVOKE",
               func= (--`INVOKE1`--), fixity=NONE},
              {def_name="UPDATE_def", fname="UPDATE",
               func= (--`UPDATE1`--), fixity=NONE},
              {def_name="SIGMA_def", fname="SIGMA",
               func= (--`SIGMA1`--), fixity=NONE},
              {def_name="HEIGHT_def", fname="HEIGHT",
               func= (--`HEIGHT1`--), fixity=NONE},
              {def_name="FV_def", fname="FV",
               func= (--`FV1`--), fixity=NONE},
              {def_name="SUB_def", fname="SUB",
               func= (--`SUB1`--), fixity=NONE},
              {def_name="FV_subst_def", fname="FV_subst",
               func= (--`FV_subst1`--), fixity=NONE},
              {def_name="SUBo_def", fname="SUBo",
               func= (--`SUB1o :^obj -> ^subs -> ^obj`--),
               fixity=SOME(Infix(NONASSOC,150))},
              {def_name="SUBd_def", fname="SUBd",
               func= (--`SUB1d :^dict -> ^subs -> ^dict`--),
               fixity=SOME(Infix(NONASSOC,150))},
              {def_name="SUBe_def", fname="SUBe",
               func= (--`SUB1e :^entry -> ^subs -> ^entry`--),
               fixity=SOME(Infix(NONASSOC,150))},
              {def_name="SUBm_def", fname="SUBm",
               func= (--`SUB1m :^method -> ^subs -> ^method`--),
               fixity=SOME(Infix(NONASSOC,150))},
              {def_name="vsubst_def", fname="/",
               func= (--`$//`--), fixity=SOME(Infix(NONASSOC,150))},
              ...
             ];
\end{verbatim}

We specify the respectfulness theorems to assist the lifting:
\begin{verbatim}

val respects =
    [OVAR1_RSP, OBJ1_RSP, INVOKE1_RSP, UPDATE1_RSP, SIGMA1_RSP,
     HEIGHT_obj1_RSP, HEIGHT_dict1_RSP, HEIGHT_entry1_RSP,
     HEIGHT_method1_RSP, FV_obj1_RSP, FV_dict1_RSP, FV_entry1_RSP,
     FV_method1_RSP, SUB1_RSP, FV_subst_RSP, vsubst1_RSP,
     SUBo_RSP, SUBd_RSP, SUBe_RSP, SUBm_RSP,
     ... ]
\end{verbatim}

We specify the polymorphic
preservation
%``definitions''
theorems to assist the lifting:
\begin{verbatim}
val polyprs = [BV_subst_PRS, COND_PRS, CONS_PRS, NIL_PRS,
               COMMA_PRS, FST_PRS, SND_PRS,
               LET_PRS, o_PRS, UNCURRY_PRS,
               FORALL_PRS, EXISTS_PRS,
               EXISTS_UNIQUE_PRS, ABSTRACT_PRS];
\end{verbatim}

We specify the polymorphic respectfulness theorems
to assist the lifting:
\begin{verbatim}
val polyrsp = [BV_subst_RSP, COND_RSP, CONS_RSP, NIL_RSP,
               COMMA_RSP, FST_RSP, SND_RSP,
               LET_RSP, o_RSP, UNCURRY_RSP,
               RES_FORALL_RSP, RES_EXISTS_RSP,
               RES_EXISTS_EQUIV_RSP, RES_ABSTRACT_RSP];
\end{verbatim}

The old theorems to be lifted are too many to list, but some will
be shown later.
\begin{verbatim}
- val old_thms = [...];
\end{verbatim}

We now define the pure sigma calculus types {\tt obj} and {\tt method},
and lift all constants and theorems:

\begin{verbatim}
- val new_thms =
      define_quotient_types
         {types = [{name = "obj",    equiv = ALPHA_obj_EQUIV},
                   {name = "method", equiv = ALPHA_method_EQUIV}],
          defs = defs,
          tyop_equivs = [LIST_EQUIV, PAIR_EQUIV],
          tyop_quotients = [LIST_QUOTIENT, PAIR_QUOTIENT,
                             FUN_QUOTIENT],
          tyop_simps = [LIST_REL_EQ, LIST_MAP_I,
                        PAIR_REL_EQ, PAIR_MAP_I,
                         FUN_REL_EQ,  FUN_MAP_I],
          respects = respects,
          poly_preserves = polyprs,
          poly_respects = polyrsp,
          old_thms = old_thms};
\end{verbatim}

The tool is able to lift many theorems to the abstract, quotient level.
Here is the original definition of substitution on a variable:
{\tt \begin{tabbing}
$\vdash$ \=($\forall$y. SUB1 [] y = OVAR1 y) $\wedge$ \\
\> ($\forall$y x c s. SUB1 ((x,c)::s) y = (if y = x then c else SUB1 s y))
\end{tabbing}}
This theorem lifts to its abstract version:
{\tt \begin{tabbing}
$\vdash$ \=($\forall$y. SUB [] y = OVAR y) $\wedge$ \\
\> ($\forall$y x c s. SUB ((x,c)::s) y = (if y = x then c else SUB s y))
\end{tabbing}}
Note how the different constants lift, e.g., {\tt SUB1} to {\tt SUB},
{\tt OVAR1} to {\tt OVAR}.  Also note that the quantification of
{\tt c:obj1} has now become of {\tt obj}.
What may not be so obvious is how the
polymorphic operators lift to the abstract versions of themselves:
{\tt []}, {\tt ,}, {\tt ::}, {\tt if...then...else}.
In fact, though the operators look the same, all the types have changed
from the lower to the higher versions.
Proving this lifted theorem took considerable automation,
hidden behind
%which may not be apparent from
the simplicity of the result.
In addition, the original theorem was not regular; before lifting,
it actually was first quietly converted to:
{\tt \begin{tabbing}
$\vdash$ \=($\forall$y. ALPHA\_obj (SUB1 [] y) (OVAR1 y)) $\wedge$ \\
\>   (\=$\forall$y x \=(c :: respects ALPHA\_obj) \\
\>\>\> (s :: respects (LIST\_REL (\$= \#\#\# ALPHA\_obj))). \\
\>\>  ALPHA\_obj (SUB1 ((x,c)::s) y) (if y = x then c else SUB1 s y))
\end{tabbing}}

Similarly, here is a version of this definition which uses the {\tt let...in}
form:
{\tt \begin{tabbing}
$\vdash$ \=($\forall$p\=\ s y. \\
\>\>  SUB1 (p::s) y = \\
\>\>  (let (x,c) = p in (if y = x then c else SUB1 s y))) $\wedge$ \\
\> ($\forall$y. SUB1 [] y = OVAR1 y)
\end{tabbing}}
This lifts to the following abstract version:
{\tt \begin{tabbing}
$\vdash$ \=($\forall$p\=\ s y. \\
\>\>  SUB (p::s) y = \\
\>\>  (let (x,c) = p in (if y = x then c else SUB s y))) $\wedge$ \\
\> ($\forall$y. SUB [] y = OVAR y)
\end{tabbing}}
In addition to the previous issues, this involves the {\tt LET}
operator, which is higher-order, taking a function as an argument.
Furthermore, because the {\tt let} involves a pair, the
pair is implemented by the {\tt UNCURRY} operator, which is also higher-order.
The following regular version was quietly proven and then lifted:
{\tt \begin{tabbing}
$\vdash$ \=($\forall$(\=p\=\ :: respects (\$= \#\#\# ALPHA\_obj)) \\
\>\>\> (s :: respects (LIST\_REL (\$= \#\#\# ALPHA\_obj))) y. \\
\>\>  AL\=PHA\_obj (SUB1 (p::s) y) \\
\>\>\>  (LE\=T \\
\>\>\>\>   (UN\=CURRY \\
\>\>\>\>\>    ($\lambda$x\=\ (c::respects ALPHA\_obj). \\
\>\>\>\>\>\>     (if y = x then c else SUB1 s y))) p)) $\wedge$ \\
\> ($\forall$y. ALPHA\_obj (SUB1 [] y) (OVAR1 y))
\end{tabbing}}

One of the most difficult theorems to lift is the induction theorem,
because it is higher-order, as it involves quantification over predicates.
{\tt \begin{tabbing}
$\vdash \forall$P\=0 P1 P2 P3. \\
\>   ($\forall$v. P0 (OVAR1 v)) $\wedge$ ($\forall$l. P2 l $\Rightarrow$ P0 (OBJ1 l)) $\wedge$ \\
\>   ($\forall$o'. P0 o' $\Rightarrow$ $\forall$s. P0 (INVOKE1 o' s)) $\wedge$ \\
\>   ($\forall$o' m. P0 o' $\wedge$ P1 m $\Rightarrow$ $\forall$s. P0 (UPDATE1 o' s m)) $\wedge$ \\
\>   ($\forall$o'. P0 o' $\Rightarrow$ $\forall$v. P1 (SIGMA1 v o')) $\wedge$ P2 [] $\wedge$ \\
\>   ($\forall$p l. P3 p $\wedge$ P2 l $\Rightarrow$ P2 (p::l)) $\wedge$ \\
\>   ($\forall$m. P1 m $\Rightarrow$ $\forall$s. P3 (s,m)) $\Rightarrow$ \\
\>   ($\forall$o'. P0 o') $\wedge$ ($\forall$m. P1 m) $\wedge$ ($\forall$l. P2 l) $\wedge$ ($\forall$p. P3 p)
\end{tabbing}}
This lifts to the abstract version:
{\tt \begin{tabbing}
$\vdash \forall$P\=0 P1 P2 P3. \\
\>   ($\forall$v. P0 (OVAR v)) $\wedge$ ($\forall$l. P2 l $\Rightarrow$ P0 (OBJ l)) $\wedge$ \\
\>   ($\forall$o'. P0 o' $\Rightarrow$ $\forall$s. P0 (INVOKE o' s)) $\wedge$ \\
\>   ($\forall$o' m. P0 o' $\wedge$ P1 m $\Rightarrow$ $\forall$s. P0 (UPDATE o' s m)) $\wedge$ \\
\>   ($\forall$o'. P0 o' $\Rightarrow$ $\forall$v. P1 (SIGMA v o')) $\wedge$ P2 [] $\wedge$ \\
\>   ($\forall$p l. P3 p $\wedge$ P2 l $\Rightarrow$ P2 (p::l)) $\wedge$ \\
\>   ($\forall$m. P1 m $\Rightarrow$ $\forall$s. P3 (s,m)) $\Rightarrow$ \\
\>   ($\forall$o'. P0 o') $\wedge$ ($\forall$m. P1 m) $\wedge$ ($\forall$l. P2 l) $\wedge$ ($\forall$p. P3 p)
\end{tabbing}}
Note how the quantifications over {\tt P0:obj1 -> bool}, etc. lift to
quantification over {\tt P0:obj -> bool}, etc.
The following regular version was quietly proven and then lifted:
{\tt \begin{tabbing}
$\vdash \forall$(\=P0\=::respects (ALPHA\_obj ===> \$=)) \\
\>\>  (P1::respects (ALPHA\_method ===> \$=)) \\
\>\>  (P2::respects (LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=)) \\
\>\>  (P3::respects ((\$= \#\#\# ALPHA\_method) ===> \$=)). \\
\>   ($\forall$v. P0 (OVAR1 v)) $\wedge$ \\
\>   ($\forall$l\=::respects (LIST\_REL (\$= \#\#\# ALPHA\_method)). \\
\>\>    P2 l $\Rightarrow$ P0 (OBJ1 l)) $\wedge$ \\
\>   ($\forall$o'::respects ALPHA\_obj. P0 o' $\Rightarrow$ $\forall$s. P0 (INVOKE1 o' s)) $\wedge$ \\
\>   ($\forall$(o'::respects ALPHA\_obj) (m::respects ALPHA\_method). \\
\>\>    P0 o' $\wedge$ P1 m $\Rightarrow$ $\forall$s. P0 (UPDATE1 o' s m)) $\wedge$ \\
\>   ($\forall$o'::respects ALPHA\_obj. P0 o' $\Rightarrow$ $\forall$v. P1 (SIGMA1 v o')) $\wedge$ \\
\>   P2 [] $\wedge$ \\
\>   ($\forall$(\=p\=::respects (\$= \#\#\# ALPHA\_method)) \\
\>\>\>   (l::respects (LIST\_REL (\$= \#\#\# ALPHA\_method))). \\
\>\>    P3 p $\wedge$ P2 l $\Rightarrow$ P2 (p::l)) $\wedge$ \\
\>   ($\forall$m::respects ALPHA\_method. P1 m $\Rightarrow$ $\forall$s. P3 (s,m)) $\Rightarrow$ \\
\>   ($\forall$o'::respects ALPHA\_obj. P0 o') $\wedge$ \\
\>   ($\forall$m::respects ALPHA\_method. P1 m) $\wedge$ \\
\>   ($\forall$l::respects (LIST\_REL (\$= \#\#\# ALPHA\_method)). P2 l) $\wedge$ \\
\>   ($\forall$p::respects (\$= \#\#\# ALPHA\_method). P3 p)
\end{tabbing}}

Finally, the most difficult theorem to lift is the function existance
theorem, after the style proposed by Gordon and Melham \cite{GoMe96}.
This uses higher-order unique existance quantification,
%with sensitive semantics.
where the unique existance is not of a simple function,
but a tuple of four functions, involving a higher-order
\quotient{} relation of tuples of functions.  This relation is {\it not\/}
an equivalence relation.
{\tt \begin{tabbing}
$\vdash$ \=$\forall$var \\
\> (obj::respects(\$= ===> LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=)) \\
\> (inv::respects(\$= ===> ALPHA\_obj ===> \$= ===> \$=)) \\
\> (\=upd::respects \\
\>\>(\$= ===> \$= ===> ALPHA\_obj ===> \$= ===> ALPHA\_method ===> \$=)) \\
\> (\=cns::respects(\$\= = ===> \$= ===> (\$= \#\#\# ALPHA\_method) ===> \\
\>\>\>             LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=)) \\
\>\>nil (par::respects(\$= ===> \$= ===> ALPHA\_method ===> \$=)) \\
\> (s\=gm::respects(\$= ===> (\$= ===> ALPHA\_obj) ===> \$=)). \\
\>\> $\exists !$\=(hom\=\_o,hom\_d,hom\_e,hom\_m)::respects \\
\>\>\>\>   (\=(ALPHA\_obj ===> \$=) \#\#\# \\
\>\>\>\>\>  (LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=) \#\#\# \\
\>\>\>\>\>  ((\$= \#\#\# ALPHA\_method) ===> \$=) \#\#\# \\
\>\>\>\>\>  (ALPHA\_method ===> \$=)). \\
\>\>\>($\forall$x. hom\_o (OVAR1 x) = var x) $\wedge$ \\
\>\>\>($\forall$d. hom\_o (OBJ1 d) = obj (hom\_d d) d) $\wedge$ \\
\>\>\>($\forall$a l. hom\_o (INVOKE1 a l) = inv (hom\_o a) a l) $\wedge$ \\
\>\>\>($\forall$a l m. hom\=\_o (UPDATE1 a l m) = \\
\>\>\>\>          upd (hom\_o a) (hom\_m m) a l m) $\wedge$ \\
\>\>\>($\forall$e d. hom\_d (e::d) = cns (hom\_e e) (hom\_d d) e d) $\wedge$ \\
\>\>\>(hom\_d [] = nil) $\wedge$ \\
\>\>\>($\forall$l m. hom\_e (l,m) = par (hom\_m m) l m) $\wedge$ \\
\>\>\>($\forall$x a. hom\=\_m (SIGMA1 x a) = \\
\>\>\>\>        sgm \=($\lambda$y. hom\_o (a <[ [(x,OVAR1 y)])) \\
\>\>\>\>\>          ($\lambda$y. a <[ [(x,OVAR1 y)]))
\end{tabbing}}
% old:
%\begin{verbatim}
%|- !var obj inv upd cns nil par sgm.
%     ?!(hom_o,hom_d,hom_e,hom_m)::respects
%                  ((ALPHA_obj ===> $=) ###
%                   (LIST_REL ($= ### ALPHA_method) ===> $=) ###
%                   (($= ### ALPHA_method) ===> $=) ###
%                   (ALPHA_method ===> $=)).
%       (!x. hom_o (OVAR1 x) = var x) /\
%       (!d. hom_o (OBJ1 d) = obj (hom_d d)) /\
%       (!a l. hom_o (INVOKE1 a l) = inv (hom_o a) l) /\
%       (!a l m. hom_o (UPDATE1 a l m) =
%                upd (hom_o a) l (hom_m m)) /\
%       (!e d. hom_d (e::d) = cns (hom_e e) (hom_d d)) /\
%       (hom_d [] = nil) /\
%       (!l m. hom_e (l,m) = par l (hom_m m)) /\
%       !x a. hom_m (SIGMA1 x a) =
%             sgm (\y. hom_o (a <[ [(x,OVAR1 y)]))
%\end{verbatim}
This lifts to the abstract version:
{\tt \begin{tabbing}
$\vdash \forall$v\=ar obj inv upd cns nil par sgm. \\
\>   $\exists !$\=(hom\_o,hom\_d,hom\_e,hom\_m). \\
\>\>   ($\forall$x. hom\_o (OVAR x) = var x) $\wedge$ \\
\>\>   ($\forall$d. hom\_o (OBJ d) = obj (hom\_d d) d) $\wedge$ \\
\>\>   ($\forall$a l. hom\_o (INVOKE a l) = inv (hom\_o a) a l) $\wedge$ \\
\>\>   ($\forall$a l m. hom\=\_o (UPDATE a l m) = \\
\>\>\>             upd (hom\_o a) (hom\_m m) a l m) $\wedge$ \\
\>\>   ($\forall$e d. hom\_d (e::d) = cns (hom\_e e) (hom\_d d) e d) $\wedge$ \\
\>\>   (hom\_d [] = nil) $\wedge$ \\
\>\>   ($\forall$l m. hom\_e (l,m) = par (hom\_m m) l m) $\wedge$ \\
\>\>   ($\forall$x a. hom\=\_m (SIGMA x a) = \\
\>\>\>           sgm \=($\lambda$y. hom\_o (a SUBo [(x,OVAR y)])) \\
\>\>\>\>             ($\lambda$y. a SUBo [(x,OVAR y)]))
\end{tabbing}}
%
% old:
%\begin{verbatim}
%|- !var obj inv upd cns nil par sgm.
%     ?!(hom_o,hom_d,hom_e,hom_m).
%       (!x. hom_o (OVAR x) = var x) /\
%       (!d. hom_o (OBJ d) = obj (hom_d d)) /\
%       (!a l. hom_o (INVOKE a l) = inv (hom_o a) l) /\
%       (!a l m. hom_o (UPDATE a l m) =
%                upd (hom_o a) l (hom_m m)) /\
%       (!e d. hom_d (e::d) = cns (hom_e e) (hom_d d)) /\
%       (hom_d [] = nil) /\
%       (!l m. hom_e (l,m) = par l (hom_m m)) /\
%       !x a. hom_m (SIGMA x a) =
%             sgm (\y. hom_o (a SUBo [(x,OVAR y)]))
%\end{verbatim}

\noindent
Note how the restricted unique existance quantification
over {\tt (hom\_o :obj1->'a,
...)}
%..., hom\_m :method1 -> 'd)}
lifts to unique existance quantification over {\tt (hom\_o :obj->'a,
...)}.
%..., hom\_m :method -> 'd)}.
To accomplish this,
the following regular version was quietly proven and then lifted:
{\tt \begin{tabbing}
$\vdash$ \=$\forall$var \\
\> (obj::respects(\$= ===> LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=)) \\
\> (inv::respects(\$= ===> ALPHA\_obj ===> \$=)) \\
\> (\=upd::respects \\
\>\>(\$= ===> \$= ===> ALPHA\_obj ===> \$= ===> ALPHA\_method ===> \$=)) \\
\> (\=cns::respects(\=\$= ===> \$= ===> (\$= \#\#\# ALPHA\_method) ===> \\
\>\>\>            LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=)) \\
\>\>nil \\
\> (par::respects (\$= ===> \$= ===> ALPHA\_method ===> \$=)) \\
\> (sgm\=::respects (\$= ===> (\$= ===> ALPHA\_obj) ===> \$=)). \\
\>\> $\exists !!$\=(hom\=\_o,hom\_d,hom\_e,hom\_m):: \\
\>\>\>\>  (ALPHA\_obj ===> \$=) \#\#\# \\
\>\>\>\>  (LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=) \#\#\# \\
\>\>\>\>  ((\$= \#\#\# ALPHA\_method) ===> \$=) \#\#\# \\
\>\>\>\>  (ALPHA\_method ===> \$=). \\
\>\>\>($\forall$x. hom\_o (OVAR1 x) = var x) $\wedge$ \\
\>\>\>($\forall$d::\=respects (LIST\_REL (\$= \#\#\# ALPHA\_method)). \\
\>\>\>\>   hom\_o (OBJ1 d) = obj (hom\_d d) d) $\wedge$ \\
\>\>\>($\forall$(a::respects ALPHA\_obj) l. \\
\>\>\>\>   hom\_o (INVOKE1 a l) = inv (hom\_o a) a l) $\wedge$ \\
\>\>\>($\forall$(a::respects ALPHA\_obj) l (m::respects ALPHA\_method). \\
\>\>\>\>   hom\=\_o (UPDATE1 a l m) = \\
\>\>\>\>\>    upd (hom\_o a) (hom\_m m) a l m) $\wedge$ \\
\>\>\>($\forall$\=(e::respects (\$= \#\#\# ALPHA\_method)) \\
\>\>\>\>(d:\=:respects (LIST\_REL (\$= \#\#\# ALPHA\_method))). \\
\>\>\>\>\> hom\_d (e::d) = cns (hom\_e e) (hom\_d d) e d) $\wedge$ \\
\>\>\>(hom\_d [] = nil) $\wedge$ \\
\>\>\>($\forall$l (\=m::respects ALPHA\_method). \\
\>\>\>\>   hom\_e (l,m) = par (hom\_m m) l m) $\wedge$ \\
\>\>\>($\forall$x (a::respects ALPHA\_obj). \\
\>\>\>\>   hom\=\_m (SIGMA1 x a) = \\
\>\>\>\>\>    sgm \=($\lambda$y. hom\_o (a <[ [(x,OVAR1 y)])) \\
\>\>\>\>\>\>      ($\lambda$y. a <[ [(x,OVAR1 y)]))
\end{tabbing}}
% old:
%\begin{verbatim}
%|- !var obj inv upd cns nil par sgm.
%     RES_EXISTS_EQUIV
%       ((ALPHA_obj ===> $=) ###
%        (LIST_REL ($= ### ALPHA_method) ===> $=) ###
%        (($= ### ALPHA_method) ===> $=) ###
%        (ALPHA_method ===> $=))
%       (\(hom_o,hom_d,hom_e,hom_m).
%          (!x. hom_o (OVAR1 x) = var x) /\
%          (!d::respects (LIST_REL ($= ### ALPHA_method)).
%             hom_o (OBJ1 d) = obj (hom_d d)) /\
%          (!(a::respects ALPHA_obj) l.
%             hom_o (INVOKE1 a l) = inv (hom_o a) l) /\
%          (!(a::respects ALPHA_obj) l (m::respects ALPHA_method).
%             hom_o (UPDATE1 a l m) = upd (hom_o a) l (hom_m m)) /\
%          (!(e::respects ($= ### ALPHA_method))
%              (d::respects (LIST_REL ($= ### ALPHA_method))).
%             hom_d (e::d) = cns (hom_e e) (hom_d d)) /\
%          (hom_d [] = nil) /\
%          (!l (m::respects ALPHA_method).
%             hom_e (l,m) = par l (hom_m m)) /\
%          !x (a::respects ALPHA_obj).
%             hom_m (SIGMA1 x a) =
%                sgm (\y. hom_o (a <[ [(x,OVAR1 y)])))
%\end{verbatim}
This automatic higher order lifting was not available before this package.

Now we have
$\mbox{\tt SIGMA}\ x\ (\mbox{\tt OVAR}\ x) =
 \mbox{\tt SIGMA}\ y\ (\mbox{\tt OVAR}\ y)$, etc., as true equality
within the HOL logic, as intended.
This accomplishes the creation of the pure sigma calculus
by identifying alpha-equivalent terms.


%
\section{Conclusions}
%
\label{conclusions}

We have implemented a package for mechanically defining higher-order
quotient types
which is a conservative, definitional extension of the HOL logic.
The package automatically lifts not only types,
but also constants and theorems from
the original level to the quotient level.

\begin{comment}
\end{comment}
Higher order quotients require
%involves
%is accomplished through
the use of \quotient{} relations,
as symmetric and transitive but not necessarily reflexive on all
%elements of
their domains.
%This is necessary to treat
%higher order quotients,
%where elements should not be compared by reflexive relations.
\begin{comment}
\end{comment}

The relationship between the lower type and the
%lifted,
quotient type
is characterized by the \quotient{} relation, the abstraction function,
and the representation function.
As a key contribution,
three necessary properties have been identified
for these to properly describe a quotient,
which are preserved in the creation of both
aggregate and higher order quotients.
Most normal polymorphic operators both respect and are preserved
across such quotients, including higher order quotients.

The Axiom of Choice was used in this design.  We showed that an alternative
design may be constructed without dependence on the Axiom of Choice, but that
it may not be extended to higher order quotients while remaining constructive.

%Most implementations of quotients in theorem provers
%provided support for
%%the modeling of
%modeling
%the quotient types,
%given an equivalence relation.
Prior to this work, only Harrison
\cite{Har98} went beyond
%this
support for modeling the quotient types
to provide automation for the lifting of constant definitions
and theorems from their original statements concerning
the original types to the corresponding analogous statements
concerning the new quotient types.  This is important
for the practical application of quotients to sizable problems like
quotients on
the syntax of
%large,
complex,
realistic programming or specification
%or annotation
%\linebreak
languages.
%The size of these grammars means that the number
%of theorems and their bulk are large, and there can be a
%significant amount of labor involved in lifting these definitions and
%theorems by hand.
These may be modelled
as recursive types, where
terms which are
partially equivalent by being
well-typed and alpha-equivalent
are identified by taking quotients.
This eases the traditional problem of the capture of bound variables
\cite{GoMe96}.

Such quotients may now be more easily modeled within a theorem prover,
using the package described here.

{\it Soli Deo Gloria.}


%\begin{appendix}
%
%%
%\section{Properties of Quotient Types}
%%
%
%Given a quotient theorem,
%%which is the defining property for the constants
%%{\it abs} and {\it rep},
%there are several tools provided in the package
%that prove and return useful derivative results.
%
%\begin{center}
%\framebox{
%\begin{tabular}[t]{l@{\hspace{0.5cm}}l}
%{\tt prove\_quotient\_rep\_abs\_equiv} & {\tt : thm -> thm} \\
%{\tt prove\_quotient\_rep\_abs\_equal} & {\tt : thm -> thm} \\
%{\tt prove\_quotient\_rep\_abs\_equal2} & {\tt : thm -> thm} \\
%{\tt prove\_quotient\_equal\_is\_rep\_equiv} & {\tt : thm -> thm} \\
%{\tt prove\_quotient\_rep\_fn\_one\_one} & {\tt : thm -> thm} \\
%{\tt prove\_quotient\_abs\_iso\_equiv} & {\tt : thm -> thm} \\
%{\tt prove\_quotient\_rep\_fn\_onto} & {\tt : thm -> thm} \\
%{\tt prove\_quotient\_abs\_fn\_onto} & {\tt : thm -> thm} \\
%{\tt prove\_quotient\_equiv} & {\tt : thm -> thm} \\
%{\tt prove\_quotient\_equiv\_refl} & {\tt : thm -> thm} \\
%{\tt prove\_quotient\_equiv\_sym} & {\tt : thm -> thm} \\
%{\tt prove\_quotient\_equiv\_trans} & {\tt : thm -> thm} \\
%\end{tabular}
%}
%\end{center}
%
%Each of these takes as its argument a quotient theorem of the form returned by
%{\tt define\_quotient\_type}:
%
%\begin{center}
%\tt
%|- (!a. {\it abs}({\it rep} a) = a) $\wedge$
%   (!r r'. {\it E\/} r r' = ({\it abs} r = {\it abs\/} r'))
%\end{center}
%
%If {\it th\/} is of this form, then evaluating
%{\tt prove\_quotient\_rep\_abs\_equiv} {\it th} proves that
%{\it rep} is the left inverse of {\it abs}, up to equivalence,
%%the representative of an equivalence class of a value
%%%the abstraction of the representative of a value
%%is equivalent to that value,
%returning the theorem:
%
%\begin{verse} \tt
%    |- !r. {\it E\/} ({\it rep} ({\it abs} r)) r
%\end{verse}
%
%%Likewise,
%Evaluating
%{\tt prove\_quotient\_rep\_abs\_equal} {\it th} proves that
%%the representative of the abstraction
%the composition of {\it rep} with {\it abs}
%of a value has the same
%equivalence class as the original value:
%
%\begin{verse} \tt
%    |- !r. {\it E\/} ({\it rep} ({\it abs} r)) = {\it E\/} r
%\end{verse}
%
%Evaluating
%{\tt prove\_quotient\_rep\_abs\_equal2} {\it th} proves
%a symmetric version of the same idea, both of which are useful
%for rewriting:
%
%\begin{verse} \tt
%    |- !r r'. {\it E\/} r ({\it rep} ({\it abs} r')) = {\it E\/} r r'
%\end{verse}
%
%Evaluating
%{\tt prove\_quotient\_equal\_is\_rep\_equiv} {\it th} proves that
%equality between abstract values is equivalence between representatives:
%
%\begin{verse} \tt
%    |- !a a'. (a = a') = {\it E\/} ({\it rep} a) ({\it rep} a')
%\end{verse}
%
%Evaluating
%{\tt prove\_quotient\_rep\_fn\_one\_one} {\it th} proves that
%{\it rep} is one-to-one:
%
%\begin{verse} \tt
%    |- !a a'. ({\it rep} a = {\it rep} a')
%              = (a = a')
%\end{verse}
%
%%Evaluating
%%{\tt prove\_quotient\_equiv\_rep\_one\_one} {\it th} proves that
%%the composition of {\it E\/} with {\it rep} is one-to-one:
%%
%%\begin{verse} \tt
%%    |- !a a'. ({\it E\/} ({\it rep} a) = {\it E\/} ({\it rep} a'))
%%              = (a = a')
%%\end{verse}
%
%Evaluating
%{\tt prove\_quotient\_abs\_iso\_equiv} {\it th} proves that
%{\it abs} and {\it E\/}
%are isomorphic with respect to equality:
%
%\begin{verse} \tt
%    |- !r r'.  ({\it abs} r = {\it abs} r')
%               = ({\it E\/} r = {\it E\/} r')
%\end{verse}
%
%Evaluating
%{\tt prove\_quotient\_rep\_fn\_onto} {\it th} proves that
%{\it rep} is onto, up to equivalence:
%
%\begin{verse} \tt
%    |- !r. ?a. {\it E\/} r ({\it rep} a)
%\end{verse}
%
%Evaluating
%{\tt prove\_quotient\_abs\_fn\_onto} {\it th} proves that
%{\it abs} is onto:
%
%\begin{verse} \tt
%    |- !a. ?r. a = {\it abs} r
%\end{verse}
%
%Evaluating
%{\tt prove\_quotient\_equiv} {\it th} proves the equivalence theorem,
%that equivalence between elements is equality between equivalence classes:
%
%\begin{verse} \tt
%    |- !x y. {\it E\/} x y = ({\it E\/} x = {\it E\/} y)
%\end{verse}
%
%Evaluating
%{\tt prove\_quotient\_equiv\_refl} {\it th} proves that
%{\it E\/} is reflexive:
%
%\begin{verse} \tt
%    |- !x. {\it E\/} x x
%\end{verse}
%
%Evaluating
%{\tt prove\_quotient\_equiv\_sym} {\it th} proves that
%{\it E\/} is symmetric:
%
%\begin{verse} \tt
%    |- !x y. {\it E\/} x y ==> {\it E\/} y x
%\end{verse}
%
%And evaluating
%{\tt prove\_quotient\_equiv\_trans} {\it th} proves
%that
%{\it E\/} is transitive:
%
%\begin{verse} \tt
%    |- !x y z. {\it E\/} x y $\wedge$
%                         {\it E\/} y z ==> {\it E\/} x z
%\end{verse}
%
%None of these functions saves anything in the current theory file.
%In fact, it should usually be unnecessary to save the results proved
%by these functions, since they can be generated quickly whenever required
%from the theorem returned by {\tt define\_quotient\_type}, which was
%itself saved.
%
%\end{appendix}


%
% ---- Bibliography ----
%
\begin{thebibliography}{5}
%
\bibitem {AbCa96}
Abadi, M., Cardelli, L.:
{\it A Theory of Objects.}
Springer-Verlag 1996.
%
\bibitem {Bar81}
Barendregt,\:H.P.:
{\it The\,Lambda\,Calculus,\,Syntax\,and\,Semantics.}
North-Holland,\:1981.
%
\bibitem {BrM92}
Bruce, K., Mitchell, J.~C.:
`PER models of subtyping, recursive types and higher-order polymorphism', in
{\it Principles of Programming Languages 19},
Albequerque, New Mexico, 1992, pp. 316-327.
%
\bibitem {CPS02}
Chicli, L., Pottier, L., Simpson C.:
`Mathematical Quotients and Quotient Types in Coq',
Proceedings of {\it TYPES 2002},
%Berg en Dal, Netherlands, April 24-28, 2002,
Lecture Notes in Computer Science, vol. 2646
(Springer-Verlag, 2002).
%
\bibitem {End77}
Enderton, H.~B.:
{\it Elements of Set Theory.}
Academic Press, 1977.
%
\bibitem {GPWZ02}
Geuvers, H., Pollack, R., Wiekijk, F., Zwanenburg, J.:
`A constructive algebraic hierarchy in Coq', in
{\it Journal of Symbolic Computation}, 34(4), 2002, pp. 271-286.
%
\bibitem {GoMe93}
Gordon, M.~J.~C., Melham, T.~F.:
{\it Introduction to HOL.}
Cambridge University Press, Cambridge, 1993.
%
\bibitem {GoMe96}
Gordon, A.~D., Melham, T.~F.:
`Five Axioms of Alpha Conversion', in
{\it Theorem Proving in Higher Order Logics:
9th International Conference, TPHOLs'96},
edited by J. von Wright, J. Grundy and J. Harrison,
Lecture Notes in Computer Science, vol. 1125
(Springer-Verlag, 1996), pp. 173-190.
%
\bibitem {Har98}
Harrison, J.:
{\it Theorem Proving with the Real Numbers,}
\S{2.11}, pp. 33-37.
Springer-Verlag 1998.
%
\bibitem {Hof95}
Hofmann, M.:
`A simple model for quotient types,' in
{\it Typed Lambda Calculus and Applications},
Lecture Notes in Computer Science, vol. 902
(Springer-Verlag, 1995), pp. 216-234.
%
%\bibitem {Hom01}
%Homeier, P.~V.:
%A Proof of the Church-Rosser Theorem
%for the Lambda Calculus
%in Higher Order Logic.
%Submitted to
%{\it
%14th International Conference on Theorem Proving in Higher Order Logics\/}
%(TPHOLs'01),
%Sept. 3-6, 2001, Edinburgh, Scotland.
%
%\bibitem {HoW01}
%Homeier, P.~V.:
%{\tt http://www.cis.upenn.edu/\verb+~+hol/lamcr}.
%
\bibitem {Kal89}
Kalker, T.: at
{\tt www.ftp.cl.cam.ac.uk/ftp/hvg/info-hol-archive/00xx/0082}.
%
\bibitem {Lei69}
Leisenring, A. C.:
{\it Mathematical Logic and Hilbert's $\varepsilon$-Symbol.}
Gordon and Breach, 1969.
%
\bibitem {Moore82}
Moore, G. H.:
{\it Zermelo's Axiom of Choice: It's Origins, Development, and Influence.}
Springer-Verlag 1982.
%
\bibitem {NiPaWe02}
Nipkow, T., Paulson, L.C., Wenzel, M.:
{\it Isabelle/HOL.}
Springer-Verlag 2002.
%
\bibitem {OwS01}
Owre, S., Shankar, N.:
{\it Theory Interpretations in PVS},
Technical Report SRI-CSL-01-01,
Computer Science Laboratory, SRI International,
Menlo Park, CA, April 2001.
%
\bibitem {Nog02}
Nogin, A.:
`Quotient Types: A Modular Approach,' in
{\it Theorem Proving in Higher Order Logics:
15th International Conference, TPHOLs 2002},
edited by V.~A.~Carre\~{n}o, C.~Mu\~{n}oz, and S.~Tahar,
Lecture Notes in Computer Science, vol. 2410
(Springer-Verlag, 2002), pp. 263-280.
%
\bibitem {LP04}
Paulson, L.:
`Defining Functions on Equivalence Classes,'
{\it ACM Transactions on Computational Logic},
in press.  Previously issued as
Report, Computer Lab, University of Cambridge, April 20, 2004.
%
\bibitem {Rob89}
Robinson, E.:
`How Complete is PER?',
in {\it Fourth Annual Symposium on Logic in Computer Science\/} (LICS),
1989, pp. 106-111.
%
\bibitem {Slo97}
Slotosch, O.:
`Higher Order Quotients and their Implementation in Isabelle HOL', in
{\it Theorem Proving in Higher Order Logics:
10th International Conference, TPHOLs'97},
edited by Elsa L. Gunter and Amy Felty,
Lecture Notes in Computer Science, vol. 1275
(Springer-Verlag, 1997), pp. 291-306.
%
\end{thebibliography}




%
\end{document}
