% 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}