1% This is quotient2.tex, the LaTeX2e file of the paper 2% "Higher Order Quotients in Higher Order Logic" 3% by Peter V. Homeier. 4\documentclass[envcountsame,runningheads]{llncs} 5\pagestyle{headings} 6\setcounter{page}{1} 7 8\usepackage{latexsym} 9\usepackage{amsmath} 10\usepackage{amssymb} 11\usepackage{verbatim} 12% 13 14% --------------------------------------------------------------------- 15% Resetting the margins. 16% --------------------------------------------------------------------- 17% \setlength{\topmargin}{0mm} 18% \setlength{\headheight}{0mm} 19% \setlength{\headsep}{0mm} 20% \setlength{\oddsidemargin}{0mm} 21% \setlength{\evensidemargin}{0mm} 22% \setlength{\textheight}{9in} 23% \setlength{\textwidth}{6.5in} 24 25% --------------------------------------------------------------------- 26% Input macros for importing EPS pictures. 27% --------------------------------------------------------------------- 28%\input boxedeps.tex %% obligatory (except for LaTeX, see below) 29%\input boxedeps.cfg %% can replace next line: 30%\SetOzTeXEPSFSpecial 31%\ShowDisplacementBoxes %%alternatives \Hide \Show 32%% \usepackage[oztex,hideboxes]{boxedeps} 33 34% --------------------------------------------------------------------- 35% Macro definitions. 36% --------------------------------------------------------------------- 37\def\fn{\hbox{$f\mkern-1.7mu n$}} 38\def\vf{\hbox{$ch$}} 39\def\ty#1{\hbox{$\hbox{\sl #1}$}} 40\def\HOL{{\small HOL}} 41\def\CCS{{\small CCS}} 42\def\CSP{{\small CSP}} 43\def\ML{{\small ML}} 44\def\LCF{{\small LCF}} 45\def\VCG{{\small VCG}} 46\def\PPL{{\small PP}{\kern-.095em}$\lambda$} 47\def\nul{\hbox{$\hbox{\bf 0}$}} 48\def\ar#1#2#3{#1 \mathbin{\stackrel{\scriptstyle #2}{\longrightarrow}} #3} 49\def\Rule#1#2{\mbox{${\displaystyle\raise 3pt\hbox{$\;\;#1\;\;$}} \over 50 {\displaystyle\lower5pt\hbox{$\;\;#2\;\;$}}$}} 51%\def\defeq{{\overset{\mathrm{def}}=}} 52\def\defeq{\stackrel{\mathrm{def}}{=}} 53 54% --------------------------------------------------------------------- 55% Macro for a tricky underbrace used later. 56% --------------------------------------------------------------------- 57\newbox\Tbox 58\def\ud{\setbox\Tbox=\hbox{$\scriptstyle\rm name\; mapping$}% 59 {\wd\Tbox=0mm\box\Tbox}} 60 61% --------------------------------------------------------------------- 62% Macros for a nice-looking `boxed figure'. 63% --------------------------------------------------------------------- 64\newlength{\rsize} 65\setlength{\rsize}{0.3mm} 66\newlength{\twidth} 67\setlength{\twidth}{\textwidth} 68\addtolength{\twidth}{-2\rsize} 69\newbox\figbox 70\long\def\Frame#1{\leavevmode 71\hbox{\vbox{\hrule height\rsize 72 \hbox{\vrule width\rsize #1\vrule width\rsize} 73 \hrule height\rsize}}} 74\def\fcaption#1{\refstepcounter{figure}\vbox{\vspace*{0mm}\hbox to\twidth{ 75 \hfil 76 Figure \thefigure: #1 \hfil}\vspace*{0mm}}} 77\def\caption#1{\refstepcounter{figure}\vbox{\vspace*{0mm}\hbox to\twidth{ 78 \hfil 79 Table \thefigure: #1 \hfil}\vspace*{0mm}}} 80%\def\fcaption#1{\refstepcounter{figure}\vbox{\vspace*{8mm}\hbox to\twidth{ 81% \hfil 82% Figure \thefigure: #1 \hfil}\vspace*{5mm}}} 83%\def\caption#1{\refstepcounter{figure}\vbox{\vspace*{8mm}\hbox to\twidth{ 84% \hfil 85% Table \thefigure: #1 \hfil}\vspace*{5mm}}} 86 87 88% ------------------------------- 89% New definitions for AMS symbols 90% ------------------------------- 91 92% 93\newcommand{\vb}{\;|\;\,} 94\newcommand{\df}{\stackrel{\Delta}{=}} 95\newcommand{\edoc}{\end{document}} 96% 97\newcommand{\lds}{\hspace*{0.2in}} 98\newcommand{\ld}[1]{\noindent\hspace*{0.2in}$#1$} 99\newcommand{\lfrac}[2]{\frac{{\textstyle #1}}{{\textstyle #2}}} 100\newcommand{\lstk}[2]{\stackrel{{\textstyle #1}}{#2}} 101\newcommand{\conequiv}{\mbox{${}^{xs} {\equiv} ^{ys}_{\alpha}$}} 102\newcommand{\conequivn}{\mbox{${\rule{0mm}{1.8ex}}^{[\;]} {\equiv}^{[\;]}_{\alpha}$}} 103\newcommand{\conequiva}[2]{\mbox{${}^{#1} {\equiv} ^{#2}_{\alpha}$}} 104%\newcommand{\conequiva}[2]{\mbox{${\rule{0mm}{1.8ex}}^{#1} {\equiv} ^{#2}_{\alpha}$}} 105\newcommand{\conequivv}[2]{\mbox{${}^{#1}_{\mathrm{var}} {\equiv} ^{#2}_{\alpha}$}} 106%\newcommand{\preserves}[8] 107%{\mbox{${#7} : {#5} \; {}^{#3}_{#1} {\equiv} ^{#4}_{#2} \; {#6} : {#8}$}} 108%\newcommand{\preserves}[8] 109%{\mbox{${#7} \leftarrow {#5} \; {}^{#3}_{#1} {\equiv} ^{#4}_{#2} \; {#6} \rightarrow {#8}$}} 110\newcommand{\preserves}[8] 111{\mbox{${#7} \succ {#5} \; {}^{#3}_{#1} {\equiv} ^{#4}_{#2} \; {#6} \prec {#8}$}} 112\newcommand{\equiva}{{\equiv}_{\alpha}} 113%\newcommand{\preservesa}[3] {\mbox{${#2} : \; {\equiv} \; {#1} : {#3}$}} 114\newcommand{\refl}[1]{\mbox{$\stackrel{\scriptscriptstyle =}{#1}$}} 115\newcommand{\itbf}[1]{\mbox{\itshape\bfseries{#1}}} 116%\newcommand{\larrow}[0]{ \twoheadrightarrow_l } 117%\newcommand{\larrow}[0]{\,\mbox{\makebox[0pt][l]{\hspace*{2.1mm}\raisebox{0.1mm}{$\shortparallel$}}$\longrightarrow$}\,} 118\newcommand{\larrow}[0]{\mathbin{\mbox{\makebox[0pt][l]{\hspace*{0.7mm}\raisebox{0.14mm}{$\shortparallel$}}$\rightarrow$}}} 119% 120\newcommand{\varl}[1]{\mbox{${#1}$}} 121\newcommand{\appl}[2]{\mbox{${#1}\;{#2}$}} 122\newcommand{\laml}[2]{\mbox{$\lambda {#1}.\;{#2}$}} 123\newcommand{\var}[1]{\mbox{${#1}$}} 124\newcommand{\app}[2]{\mbox{${#1}\;{#2}$}} 125\newcommand{\lam}[2]{\mbox{$\lambda {#1}.\;{#2}$}} 126\newcommand{\presim}[0]{\mbox{$\mbox{\tt \$}\mathbin{\sim}$}} 127 128% -------------------- 129% Symbols and keywords 130% -------------------- 131 132\newcommand{\vvsub}{\mathrel{{//}_v}} 133\newcommand{\mybigcup}{\mathop{\displaystyle\bigcup}\limits} 134\newcommand{\mycross}{\mbox{$\;\times\;$}} 135\newcommand{\mynot}{\mathop\sim} 136\newcommand{\mydiv}{\mathrel{\bf div}} 137%\newcommand{\cond}{\mbox{\tt \ => }} 138%\newcommand{\alt}{\mbox{\tt \ | }} 139\newcommand{\cond}{\mbox{\tt $\; => \;$}} 140\newcommand{\alt}{\mbox{\tt $\; \mid \;$}} 141%%\newcommand{\cond}{\mbox{\tt \; => \;}} 142%%\newcommand{\alt}{\mbox{\tt \; | \;}} 143\newcommand{\ldash}{\mbox{$\;$---$\;$}} 144\newcommand{\append}{\mathbin{\&}} 145\newcommand{\arrowx}{\mbox{$\;$---$\!\!\times\;$}} 146\newcommand{\goal}{\mbox{?--}} 147\newcommand{\Source}{\mbox{\sf Source}} 148\newcommand{\Target}{\mbox{\sf Target}} 149\newcommand{\Ssem}{\mbox{\sf Ssem}} 150\newcommand{\Tsem}{\mbox{\sf Tsem}} 151\newcommand{\goesto}[1]% 152{\mbox{$\;\,\Longrightarrow_{\scriptscriptstyle #1}\,\;$}} 153\newcommand{\pgoesto}[1]% 154{\mbox{$\Longrightarrow_{\scriptscriptstyle #1}$}} 155\newcommand{\myd}{\,\underline{\diamond}\,} 156\newcommand{\like}[2]{\mbox{$#1\;\mbox{like}\;#2$}} 157\newcommand{\lb}{\mbox{$[\![$}} 158\newcommand{\rb}{\mbox{$]\!]$}} 159\newcommand{\quotient}{partial equivalence} 160\newcommand{\Quotient}{Partial Equivalence} 161%\newcommand{\repofabs}{\mbox{\tt //}} 162\newcommand{\repofabs}{\Downarrow} 163 164% ------------------------- 165% Theorem environments 166% ------------------------- 167 168%\newtheorem{atheorem}{Theorem} 169%\newtheorem{alemma}[atheorem]{Lemma} 170%\newtheorem{adefinition}[atheorem]{Definition} 171 172% --------------------------------------------------------------------- 173% Start of document 174% --------------------------------------------------------------------- 175 176\begin{document} 177 178 179\title{Higher Order Quotients in Higher Order Logic} 180 181\titlerunning{Higher Order Quotients in Higher Order Logic} 182 183\author{Peter~V.~Homeier} 184 185\authorrunning{Peter~V.~Homeier} 186 187\institute{ 188U. S. Department of Defense 189\\ 190palantir@trustworthytools.com 191\\ 192http://www.trustworthytools.com 193} 194 195\maketitle 196 197\begin{abstract} 198The quotient operation is a standard feature of set theory, where 199a set is partitioned into subsets by an equivalence relation. 200% the resulting subsets of equivalent elements are called equivalence classes. 201We reinterpret this idea for Higher Order Logic (HOL), where types are 202divided by an equivalence relation to create new types, called 203quotient types. 204We present a tool for the Higher Order Logic theorem prover 205to mechanically construct quotient types as 206new types in the HOL logic, 207and to automatically lift constants and 208theorems about the original types 209to corresponding constants and theorems about the quotient types. 210%Tools are also provided to create quotients of aggregate types, 211%in particular lists, pairs, sums, options, and function types. 212This package exceeds the functionality of Harrison's package, 213creating quotients of multiple mutually recursive types simultaneously, 214and supporting the equivalence of aggregate types, such as lists and pairs. 215Most importantly, 216this package successfully 217creates higher-order quotients, automatically lifting 218theorems with quantification over functions 219%on the quotient types 220of any higher order. 221% which to our knowledge has never been done before. 222This is accomplished through the 223%novel introduction 224%key innovation 225use 226of {\it \quotient{} relations}, 227a possibly nonreflexive version of equivalence relations. 228We demonstrate this tool by lifting Abadi and Cardelli's sigma calculus. 229\end{abstract} 230 231 232% 233\section{Introduction} 234% 235 236The quotient operation is a standard feature of mathematics, 237including set theory and abstract algebra. It provides a way to 238cleanly identify elements that previously were distinct. 239This simplifies the system by removing unneeded structure. 240%A system that discriminates between elements 241%which are considered equivalent but not identical 242%before the quotient operation thus gives rise to a system that identifies 243%such equivalent elements so that they can no longer be distinguished. 244 245Traditionally, quotients have found many applications. 246Classic examples are the construction 247of the integers from pairs of non-negative natural numbers, 248or 249%the construction of 250the rationals from pairs of integers. 251In the lambda calculus \cite{Bar81} and similar calculi, it is 252common to identify terms which are alpha-equivalent, that differ only by 253the choice of local names used by binding operators. 254Other examples include the construction of bags from lists by ignoring order, 255%where the order does not matter, 256and the construction of sets from bags by ignoring duplicates. 257%where if positive, the number of equal elements does not matter. 258 259The ubiquity of quotients has recommended their investigation 260%Since quotients are ubiquitous, 261%they have been previously investigated 262within the field of mechanical theorem proving. 263The first to appear was Ton Kalker's 1989 package for HOL88 \cite{Kal89}. 264Isabelle/HOL 265\cite{NiPaWe02} 266has mechanical support for the creation of 267higher order quotients by Oscar Slotosch \cite{Slo97}, 268using partial equivalence relations represented as a type class, 269with equivalence relations as a subclass. 270That system provides a definitional framework for establishing 271quotient types, including higher order. 272Independently, Larry Paulson has shown a construction of first-order quotients 273in Isabelle without any use of the Hilbert choice operator 274\cite{LP04}. 275PVS uses quotients to support theory interpretations \cite{OwS01}. 276MetaPRL has quotients in its foundations, 277as a type with a new equality \cite{Nog02}. 278Coq, based on the Calculus of Constructions \cite{Hof95}, 279supports quotients \cite{GPWZ02} but 280has some difficulties with higher order 281\cite{CPS02}. 282These systems provide little automatic support. 283In particular, there is no automatic lifting of constants or theorems. 284 285John Harrison has developed a package for the 286%Higher Order Logic 287HOL 288theorem prover which supports first order quotients, 289including automation to define new quotient types 290%based on an existing type and an equivalence relation on that type, 291and to lift to the quotient level both constants 292and theorems previously established 293\cite{Har98}. 294% 295This automatic lifting is key to practical support for quotients. 296A quotient of a group 297would be incomplete without also mapping the original group 298operation to a corresponding one for the quotient group. 299%Similarly, theorems about the group 300%which are independent of the equivalence relation 301Similarly, a theorem stating that the original group was abelian 302should also be true of the quotient group. 303%If one wished to take a quotient of a group, it would be inadequate to 304%only create the quotient set of the original set by the equivalence relation, 305%without appropriately mapping the original group operation to a corresponding 306%group operation for the new quotient set. Similarly, any theorems 307%describing properties of the original group 308%which are independent of the equivalence relation 309%should also be true (in a translated form) of the new quotient group. 310Mechanizing this lifting is vital for avoiding the repetition of proofs 311at the higher level which were already proved at the lower level. 312Such automation is not only practical, but mathematically incisive. 313%Such automation makes the quotient operation more practical and intellectually cogent. 314 315Despite the quality of Harrison's excellent package, it does have 316limitations. It can only lift one type at a time, 317and does not deal with aggregate types, such as lists or pairs 318involving types being lifted, 319which makes it difficult to lift a family of mutually nested recursive types. 320%Also, it does not deal with aggregate types, such as when some 321%points of a mutual recursion involve the type operators (e.g., {\tt ('a)list}). 322Most importantly, it is limited to lifting only first order theorems, 323where 324%universal and existential 325quantification is permitted over the 326type being lifted, but not over functions or predicates involving the type 327being lifted. 328 329In this paper we describe a new package for quotients for the Higher Order 330Logic theorem prover that meets these three concerns. It provides a tool 331for lifting multiple types across multiple equivalence relations simultaneously. 332Aggregate equivalence relations are produced and used automatically. 333Most significantly, this package supports the automatic 334lifting of theorems that involve higher order functions, including 335quantification, of any finite order. 336This is possible through the use of 337{\it \quotient{} relations} 338\cite{Rob89}, 339as a possibly non-reflexive variant of 340equivalence relations, enabling 341%the creation of 342quotients 343%relationships 344of function types. 345%rather than just simple or aggregate types. 346%We introduce a new definition of when one type is a quotient of another, 347%based on three properties that relate a \quotient{} relation to its 348The relationship between these \quotient{} relations and their 349associated abstraction and representation functions (mapping between the 350lower and higher types) 351is expressed in {\it quotient theorems\/} which 352play a central and vital role in this package. 353 354The precise definition of the quotient relationship between the 355original and lifted types, and the proof of that relationship's 356preservation 357for a function type, 358%given \quotient{} relations 359given existing quotients 360for the function's domain and range, are the heart of this paper, 361and are presented in full detail. 362These 363%definition and proof 364form the core theory that 365justifies the treatment of all higher order functions, 366including higher order 367universal, existential, and unique existential quantification. 368 369In addition, many existing polymorphic operators from the theories of 370lists, pairs, sums, and options have theorems pre-proven 371showing the operators' respectfulness of equivalence relations and 372their preservation across quotients, yielding results at the 373quotient level which correspond properly with their results at the lower level. 374These respectfulness and preservation theorems enable the automatic 375lifting of theorems that mention these operators. Additional operators 376can also be lifted by proving 377and including 378the corresponding respectfulness and preservation 379theorems, which justify the operator's use across quotients. 380%operations. 381 382The system is thus extensible, both in terms of new operators, and even 383in terms of new polymorphic type operators, by proving and including 384theorems entailing 385%the existence of 386a quotient 387of the type operator, 388given quotients 389of the 390argument types. 391%types which are arguments of the operator. 392 393The structure of this paper is as follows. In section \ref{quotientsets} 394we briefly review quotient sets. In section \ref{quotienttypes} we 395re-interpret this idea for type theory. 396Section \ref{equivalence} discusses equivalence relations and their 397aggregates. 398Section \ref{quotientrelation} describes \quotient{} relations, 399their extension for aggregate and function types, 400the properties of a quotient relationship, 401and quotient extension theorems 402for lifting aggregate and function types. 403%%In particular, 404%The quotient extension theorem for function types 405%is the heart of higher order quotients, and 406%%its proof is presented 407%is proved 408%in section \ref{condquotients}. 409Section \ref{axiomofchoice} describes an alternative design 410that avoids use of the Axiom of Choice. 411Section \ref{liftingall} presents 412the main tool of the quotient package, which lifts types, constants, 413and theorems across the quotients. 414The next several sections discuss 415its work 416%the work of the main tool of section \ref{liftingall} 417in more detail. 418Section \ref{newquotienttype} 419describes the definition of new quotient types, and 420section \ref{liftingdefs} describes the definition of lifted versions 421of constants. 422Section \ref{liftingtheorems} describes the various input theorems needed by 423the tool to automatically lift theorems. 424%from the lower level to the quotient level. 425Section \ref{restrictions} describes the restrictions on theorems 426in order for them to lift properly, and section 427\ref{nonstandard} loosens these restrictions, 428helpfully attempting to lift even some improper theorems. 429%describing how the 430%package will try to generate the proper theorem to lift 431%even given an improper one. 432%even if the given lower theorem is not proper. 433Section \ref{liftingsets} discusses lifting theorems about sets. 434In sections \ref{sigmacalculus} through 435\ref{puresigmacalculus}, we present Abadi and Cardelli's sigma calculus 436\cite{AbCa96}, 437its formulation in HOL and its lifting by quotients over alpha-equivalence. 438Finally, our conclusions are presented in section \ref{conclusions}. 439 440We are grateful for the helpful comments and 441suggestions made by 442Rob Arthan, 443Randolph Johnson, 444Sylvan Pinsky, 445Yvonne V. Shashoua, 446and 447Konrad Slind, 448%which have greatly improved this paper. 449and especially Michael Mislove for identifying 450partial equivalence relations and 451William Schneeberger for the key idea in the proof of theorem 452\ref{partinverses}. 453 454 455% 456\section{Quotient Sets} 457% 458\label{quotientsets} 459 460Quotient sets are a standard construction of set theory. 461They have found wide application in many areas of mathematics, 462including algebra and logic. 463The following description is abstracted from \cite{End77}. 464 465A binary relation 466$\sim$ 467on $S$ is 468an {\it equivalence relation\/} 469if it is reflexive, symmetric, and transitive. 470$$ 471\begin{array}{l@{\hspace{0.6cm}}l@{\hspace{0.3cm}}l} 472\mbox{\it reflexive:} & 473\forall x \in S. & x \sim x \\ 474\mbox{\it symmetric:} & 475\forall x,y \in S. & x \sim y \ \Rightarrow \ y \sim x \\ 476\mbox{\it transitive:} & 477\forall x,y,z \in S. & x \sim y \ \wedge \ y \sim z \ \Rightarrow \ x \sim z 478\end{array} 479$$ 480Let $\sim$ be an equivalence relation. 481Then the {\it equivalence class\/} of $x$ ({\it modulo\/} $\sim$) 482is defined as $[ x ]_{\sim} \defeq \{ y \ | \ x \sim y \}$. 483It follows \cite{End77} that 484$$ 485[ x ]_{\sim} = [ y ]_{\sim} \ \ \Leftrightarrow \ \ x \sim y . 486$$ 487 488\noindent 489The {\it quotient set\/} $S / \mathbin{\sim}$ is defined as 490%is defined as the set of equivalence classes of elements of $S$. 491$$ 492S / \mathbin{\sim} \ \defeq \ \{ [ x ]_{\sim} \ | \ x \in S \}. 493$$ 494\noindent 495This is the set of all equivalence classes modulo $\sim$ of elements in $S$. 496 497%A {\it partition\/} $\Pi$ of a set $S$ is a set of nonempty subsets of $S$ 498%that is disjoint and exhaustive. 499%Then 500%$S / \mathbin{\sim}$ is a partition of $S$ 501%\cite{End77}. 502 503 504% 505\section{Equivalence Relations and Equivalence Theorems} 506% 507\label{equivalence} 508 509%Quotient sets \cite{End77} are a standard construction of set theory. 510%%They have found wide application in many areas of mathematics, 511%%including algebra and logic. 512% 513%We reinterpret quotient sets 514%\cite{End77} 515%for the Higher Order Logic theorem prover 516%\cite{GoMe93}, 517%whose logic is a type theory, rather than a set theory. 518% 519Before considering quotients, we examine equivalence relations, 520on which such traditional quotients as those mentioned in the introduction 521have been based. 522 523Let $\tau$ be any type. A binary relation $R$ on $\tau$ can be 524represented in HOL as a curried function 525of type $\tau \rightarrow (\tau \rightarrow \mbox{\tt bool})$. 526We will take advantage of the curried nature of $R$, where 527$R\ x\ y = (R\ x)\ y$. 528 529An equivalence relation is a binary relation $E$ satisfying 530$$ 531\begin{array}{l@{\hspace{0.6cm}}l@{\hspace{0.3cm}}l} 532\mbox{\it reflexivity:} & 533\forall x:\tau . & E\ x\ x \\ 534\mbox{\it symmetry:} & 535\forall x\ y :\tau. & E\ x\ y \ \Rightarrow \ E\ y\ x \\ 536\mbox{\it transitivity:} & 537\forall x\ y\ z:\tau. & E\ x\ y \ \wedge \ E\ y\ z \ \Rightarrow \ E\ x\ z 538\end{array} 539$$ 540 541These three properties are encompassed in 542%one, which we call 543the {\it equivalence property:} 544$$ 545%\begin{array}[t]{l@{\hspace{0.5cm}}l@{\hspace{1.5cm}}} 546\begin{array}[t]{l@{\hspace{0.6cm}}l@{\hspace{0.3cm}}} 547\mbox{\it equivalence:} & 548\mbox{\tt EQUIV}\ E \ \defeq \ 549\forall x\ y :\tau.\ E\ x\ y \ \Leftrightarrow \ (E\ x = E\ y) 550\end{array} 551$$ 552 553\noindent 554A theorem of the form 555$\vdash$ {\tt EQUIV} $E$ 556%($E : \tau$ {\tt ->} $\tau$ {\tt -> bool}) 557is called an {\it equivalence theorem\/} on type $\tau$. 558 559Given an equivalence theorem, we can obtain the reflexive, symmetric, 560and transitive properties, or given those three, construct the corresponding 561equivalence theorem, using the following Standard ML functions of our package. 562\begin{center} 563\framebox{ 564\begin{tabular}[t]{rl} 565{\tt equiv\_refl} & {\tt : thm -> thm} \\ 566{\tt equiv\_sym} & {\tt : thm -> thm} \\ 567{\tt equiv\_trans} & {\tt : thm -> thm} \\ 568{\tt refl\_sym\_trans\_equiv} & {\tt : thm -> thm -> thm -> thm} \\ 569\end{tabular} 570} 571\end{center} 572 573% 574\subsection{Equivalence Extension Theorems} 575% 576\label{condequivs} 577 578Given an equivalence relation 579%{\it E\/}{\tt :ty} $\rightarrow$ {\tt ty} $\rightarrow$ {\tt bool} 580$E:\tau \rightarrow \tau \rightarrow \mbox{\tt bool}$ 581on values of type $\tau$, 582there is a natural extension of {\it E\/} to values of lists of $\tau$. 583This is expressed as {\tt LIST\_REL\;{\it E\/}}, 584which forms an equivalence relation of type 585%{\tt (ty)list} $\rightarrow$ {\tt (ty)list} $\rightarrow$ {\tt bool}. 586$\tau\ \mbox{\tt list} \rightarrow \tau\ \mbox{\tt list} \rightarrow \mbox{\tt bool}$. 587Similarly, equivalence relations on pairs, sums, and options 588may be formed 589%in the HOL logic 590from their constituent types' equivalence relations by the following operators. 591 592\begin{center} 593\framebox{ 594\begin{tabular}[t]{lrl} 595Type & Operator \ \ \ \ \ & Type of operator \\ 596\hline \\ 597%identity & {\tt = : } & {\tt 'a -> 'a -> bool} \\ 598list & {\tt LIST\_REL : } & {\tt ('a -> 'a -> bool) ->} \\ 599& & {\tt \ \ \ \ \ \ 'a list -> 'a list -> bool} \\ 600pair & {\tt \#\#\# : } & {\tt ('a -> 'a -> bool) -> ('b -> 'b -> bool) ->} \\ 601& & {\tt \ \ \ \ \ \ 'a \# 'b -> 'a \# 'b -> bool} \\ 602sum & {\tt +++ : } & {\tt ('a -> 'a -> bool) -> ('b -> 'b -> bool) ->} \\ 603& & {\tt \ \ \ \ \ \ 'a + 'b -> 'a + 'b -> bool} \\ 604option\ \ & {\tt OPTION\_REL : } & {\tt ('a -> 'a -> bool) ->} \\ 605& & {\tt \ \ \ \ \ \ 'a option -> 'a option -> bool} \\ 606% fun & {\tt ===> : } & {\tt ('a -> 'a -> bool) -> ('b -> 'b -> bool) ->} \\ 607% & & {\tt \ \ \ \ \ \ ('a -> 'b) -> ('a -> 'b) -> bool} \\ 608\end{tabular} 609} 610\end{center} 611 612These operators are defined 613as indicated below. 614 615\begin{definition} 616\label{listrel} 617$\begin{array}[t]{lcccl} 618\mbox{\tt LIST\_REL}\ R & \mbox{\tt []} & \mbox{\tt []} & \ = \ & \mbox{\bf true} \\ 619\mbox{\tt LIST\_REL}\ R & (a \mbox{\tt ::} as) & \mbox{\tt []} & \ = \ & \mbox{\bf false}\\ 620\mbox{\tt LIST\_REL}\ R & \mbox{\tt []} & (b \mbox{\tt ::} bs) & \ = \ & \mbox{\bf false}\\ 621\mbox{\tt LIST\_REL}\ R & (a \mbox{\tt ::} as) & (b \mbox{\tt ::} bs) & \ = \ 622 & R\ a\ b\ \wedge \mbox{\tt LIST\_REL}\ R\ as\ bs 623\end{array}$ 624\end{definition} 625 626\begin{definition} 627\label{pairrel} 628$\begin{array}[t]{lcccl} 629(R_1\ \mbox{\tt \#\#\#}\ R_2) & (a_1, a_2) & (b_1, b_2) & \ = \ 630 & R_1\ a_1\ b_1 \ \wedge \ R_2\ a_2\ b_2 631\end{array}$ 632\end{definition} 633 634\begin{definition} 635\label{sumrel} 636$\begin{array}[t]{lcccl} 637(R_1\ \mbox{\tt +++}\ R_2) & (\mbox{\tt INL}\ a_1) & (\mbox{\tt INL}\ b_1) & \ = \ 638 & R_1\ a_1\ b_1 \\ 639(R_1\ \mbox{\tt +++}\ R_2) & (\mbox{\tt INL}\ a_1) & (\mbox{\tt INR}\ b_2) & \ = \ 640 & \mbox{\bf false} \\ 641(R_1\ \mbox{\tt +++}\ R_2) & (\mbox{\tt INR}\ a_2) & (\mbox{\tt INL}\ b_1) & \ = \ 642 & \mbox{\bf false} \\ 643(R_1\ \mbox{\tt +++}\ R_2) & (\mbox{\tt INR}\ a_2) & (\mbox{\tt INR}\ b_2) & \ = \ 644 & R_2\ a_2\ b_2 645\end{array}$ 646\end{definition} 647 648\begin{definition} 649\label{optionrel} 650$\begin{array}[t]{lcccl} 651\mbox{\tt OPTION\_REL}\ R & \mbox{\tt NONE} & \mbox{\tt NONE} & \ = \ 652 & \mbox{\bf true} \\ 653\mbox{\tt OPTION\_REL}\ R & (\mbox{\tt SOME}\ a) & \mbox{\tt NONE} & \ = \ 654 & \mbox{\bf false} \\ 655\mbox{\tt OPTION\_REL}\ R & \mbox{\tt NONE} & (\mbox{\tt SOME}\ b) & \ = \ 656 & \mbox{\bf false} \\ 657\mbox{\tt OPTION\_REL}\ R & (\mbox{\tt SOME}\ a) & (\mbox{\tt SOME}\ b) & \ = \ 658 & R\ a\ b 659\end{array}$ 660\end{definition} 661 662They 663%operators 664take 665%one or two 666arguments which are the 667equivalence relations for component subtypes, and return 668an equivalence relation for the aggregate type. 669 670Since the pair and sum relation operators have two arguments, 671they are infix, whereas the list and option relation operators 672are unary, prefix operators. 673The operator definitions 674may be needed to prove respectfulness 675(see \S \ref{respectfulness}, \ref{polyrespects}). 676 677Given equivalence theorems for the constituent subtypes, the 678equivalence theorems for the natural extensions to aggregate types (e.g., 679lists, pairs, sums, and options) may be created by the following 680SML functions of our package. 681 682\begin{center} 683\framebox{ 684\begin{tabular}[t]{rl} 685{\tt list\_equiv} & {\tt : thm -> thm} \\ 686{\tt pair\_equiv} & {\tt : thm -> thm -> thm} \\ 687{\tt sum\_equiv} & {\tt : thm -> thm -> thm} \\ 688{\tt option\_equiv} & {\tt : thm -> thm} \\ 689\\ 690{\tt identity\_equiv} & {\tt : hol\_type -> thm} \\ 691{\tt make\_equiv} & {\tt : thm list -> hol\_type -> thm} \\ 692\end{tabular} 693} 694\end{center} 695 696{\tt identity\_equiv} {\it ty\/} creates the trivial equivalence theorem for 697the given type {\it ty,} using equality ({\tt =}) as the equivalence relation. 698 699{\tt make\_equiv} {\it equivs ty\/} creates an equivalence 700theorem for the given type {\it ty,} 701which may be a complex type expression with lists, pairs, etc. 702Here {\it equivs} is a list of both equivalence theorems 703for the base types and equivalence extension theorems for type operators 704(see section \ref{condequivs}). 705 706{\it Equivalence extension theorems\/} for type operators 707%as: 708have the form: 709\begin{center} 710\begin{tabular}{rl} 711$\vdash$ & {\tt $\forall$E1 ... En. } \\ 712& {\tt ($\forall$(x:$\alpha_1$) (y:$\alpha_1$). E1 x y $\Leftrightarrow$ (E1 x = E1 y)) $\Rightarrow$} 713% \\ 714%& {\tt ...} \\ 715 {\tt ...} \\ 716& {\tt ($\forall$(x:$\alpha_n$) (y:$\alpha_n$). En x y $\Leftrightarrow$ (En x = En y)) $\Rightarrow$} \\ 717& {\tt ($\forall$(x:$(\alpha_1,...,\alpha_n)op$) (y:$(\alpha_1,...,\alpha_n)op$).} \\ 718& \hspace{4mm} 719{\tt OP\_REL E1 ... En x y $\Leftrightarrow$ } \\ 720& {\tt 721\hspace{5mm} 722(OP\_REL E1 ... En x = OP\_REL E1 ... En y))} \\ 723\end{tabular} 724\end{center} 725 726Given the type operator $(\alpha_1,...,\alpha_n)op$, 727{\tt OP\_REL} should be an operator which takes $n$ arguments, 728which are the equivalence relations {\tt E1} through {\tt En} 729on the types $\alpha_1$ through $\alpha_n$, 730%and yields 731yielding 732an equivalence relation for the type $(\alpha_1,...,\alpha_n)op$. 733 734Using the above relation extension operators, 735the aggregate type operators {\tt list}, 736{\tt prod}, 737{\tt sum}, and 738{\tt option} 739%{\tt ($\alpha$)list}, 740%{\tt ($\alpha$)option}, 741%{\tt ($\alpha,\beta$)prod}, and 742%{\tt ($\alpha,\beta$)sum} 743have the following equivalence extension theorems: 744 745\vspace{3mm} 746 747\noindent 748{\tt 749\begin{tabular}{ll} 750LIST\_EQUIV: & 751 $\vdash \forall E.\ \mbox{\tt EQUIV}\ E \;\Rightarrow \;\mbox{\tt EQUIV}\;(\mbox{\tt LIST\_REL}\ E)$ \\ 752%\\ 753PAIR\_EQUIV: & 754 $\vdash \forall E_1\ E_2.\ \mbox{\tt EQUIV}\ E_1 \;\Rightarrow \; 755 \mbox{\tt EQUIV}\ E_2 \;\Rightarrow \; 756 \mbox{\tt EQUIV}\;(E_1\ \mbox{\tt \#\#\#}\ E_2)$ \\ 757% $\vdash \forall E_1\ E_2.$ EQUIV $E_1$ $\Rightarrow$ EQUIV $E_2$ $\Rightarrow$ 758% EQUIV\;($E_1$ \#\#\# $E_2$) \\ 759%\\ 760SUM\_EQUIV: \ & 761 $\vdash \forall E_1\ E_2.\ \mbox{\tt EQUIV}\ E_1 \;\Rightarrow \; 762 \mbox{\tt EQUIV}\ E_2 \;\Rightarrow \; 763 \mbox{\tt EQUIV}\;(E_1\ \mbox{\tt +++}\ E_2)$ \\ 764% $\vdash \forall E_1\ E_2.$ EQUIV $E_1$ $\Rightarrow$ EQUIV $E_2$ $\Rightarrow$ 765% EQUIV\;($E_1$ +++ $E_2$) \\ 766%\\ 767OPTION\_EQUIV: & 768 $\vdash \forall E.\ \mbox{\tt EQUIV}\ E \;\Rightarrow \;\mbox{\tt EQUIV}\;(\mbox{\tt OPTION\_REL}\ E)$ \\ 769% $\vdash \forall E$. EQUIV $E$ $\Rightarrow$ EQUIV\;(OPTION\_REL $E$) \\ 770\end{tabular} 771} 772 773 774% 775\section{Partial Equivalence Relations and Quotient Theorems} 776% 777\label{quotientrelation} 778 779In this section we introduce a new definition of the quotient 780relationship, based on {\it \quotient{} relations} 781(PERs), related to but different from equivalence relations. 782%a related but different concept than equivalence relations. 783Every equivalence relation is a \quotient{} relation, but 784not every \quotient{} relation is an equivalence relation. 785An equivalence relation is reflexive, symmetric and transitive, 786while a \quotient{} relation is symmetric and transitive, but not 787necessarily reflexive on all of its domain. 788 789Why use \quotient{} relations with a weaker reflexivity condition? 790The reason involves forming quotients of higher order types, that is, 791functions whose domains or ranges involve types being lifted. Unlike lists 792and pairs, the equivalence relations for the domain and range do not 793naturally extend to a useful equivalence relation for functions 794from the domain to the range. 795 796The reason is that not all functions which are elements of the function 797type are {\it respectful\/} of the associated equivalence relations, 798as described in 799section {\ref{respectfulness}}. 800For example, given an equivalence relation 801$E:\tau \rightarrow \tau \rightarrow \mbox{\tt bool}$, 802the set of functions from $\tau$ to $\tau$ may contain a function 803$f^?$ where for some $x$ and $y$ 804%of type $\tau$ 805which are equivalent 806($E\ x\ y$), the results of $f^?$ are not equivalent 807($\neg (E\ (f^?\ x)\ (f^?\ y))$). 808Such disrespectful functions cannot be worked with; they do not 809correspond to any function at the abstract quotient level. 810% 811Suppose instead that $f^?$ did lift. 812Let $\lceil \phi \rceil$ be the lifted version of $\phi$. 813As $\lceil f^? \rceil$ is the lifted version of $f^?$, 814it should act just like $f^?$ on its argument, 815except that it should not consider the lower level details 816that $E$ 817%and thus $\lceil \_ \rceil$ 818disregards. 819%collapses. 820%obscures. 821Thus 822%Because we assume that $f^?$ lifts, 823$ 824\forall u.\ 825\lceil f^? \rceil \lceil u \rceil = 826\lceil f^?\ u \rceil $. 827%This means that the lifted version of $f^?$ must act on lifted versions 828%of its argument just as if the original $f^?$ had been applied to the 829%original argument, and the result lifted. 830Then 831certainly 832$\forall u\ v.\ E\ u\ v \Leftrightarrow (\lceil u \rceil = \lceil v \rceil)$, 833and 834because $E\ x\ y$, we must have $\lceil x \rceil = \lceil y \rceil$. 835Applying $\lceil f^? \rceil$ to both sides, 836$\lceil f^? \rceil \lceil x \rceil = \lceil f^? \rceil \lceil y \rceil$. 837But this implies $\lceil f^?\ x \rceil = \lceil f^?\ y \rceil$, 838which means that $E\ (f^?\ x)\ (f^?\ y)$, which we have said is false, 839a contradiction. 840% 841\begin{comment} 842%Every theorem at the quotient level should correspond to a theorem at 843%the lower level. 844Any equivalence relation $E^2$ for the function type 845$\tau \rightarrow \tau$ 846would 847have to be reflexive, so we would have $E^2\ f^?\ f^?$. 848%which with $E\ x\ y$ would {\it not\/} imply $E (f^? x) (f^? y)$. 849But this would invalidate 850%{\tt ?- \verb+~+(?f1 f2 x. $E^2$ f1 f2 $\wedge$ \verb+~+$E$ (f1 x) (f2 x)}, 851%{\tt ?- !f1 f2 x. $E^2$ f1 f2 $\Rightarrow$ $E$ (f1 x) (f2 x)} 852%(take ${\tt f1}\ z = f^? x$, and ${\tt f2}\ z = f^? y$), 853%$\forall f_1 f_2\ x.\ E^2 f_1 f_2 \Rightarrow E (f_1\ x) (f_2\ x)$ 854%$\forall f_1 f_2\ x\ y.\ E^2 f_1 f_2 \wedge E\ x\ y \Rightarrow 855%$\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)$, 856%$\forall f, g, x, y.\ E^2 f g \wedge E\ x\ y \Rightarrow E (f\ x) (g\ y)$, 857%$\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)$, 858$\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)$, 859%the lower unlifted version of 860%to be lifted to 861the higher version of which is 862%the true 863%{\tt |- \verb+~+(?f1 f2 x. f1 = f2 $\wedge$ \verb+~+(f1 x = f2 x)}, 864%{\tt |- !f1 f2 x. f1 = f2 $\Rightarrow$ (f1 x = f2 x)}, 865%$\forall f_1 f_2\ x.\ (f_1 = f_2) \Rightarrow (f_1\ x = f_2\ x)$, 866%$\forall f_1 f_2\ x\ y.\ (f_1 = f_2) \wedge (x = y) \Rightarrow (f_1\ x = f_2\ y)$, 867%$\forall f_1, f_2, x, y.\ (f_1 = f_2) \wedge (x = y) \Rightarrow (f_1\ x = f_2\ y)$, 868%$\forall f_1\,f_2\, x\,y.\ f_1 = f_2 \wedge x = y \Rightarrow f_1\ x = f_2\ y$, 869%$\forall f, g, x, y.\ f = g \wedge x = y \Rightarrow f\ x = g\ y$, 870%$\forall f_1, f_2, x, y.\ f_1 = f_2 \wedge x = y \Rightarrow f_1\ x = f_2\ y$, 871$\forall f_1\;f_2\;x\;y.\;f_1 = f_2 \wedge x = y \Rightarrow f_1\;x = f_2\;y$, 872which is obviously true. 873%Every theorem at the higher level should correspond to a theorem at the lower level. 874%Every provable statement at the higher level should translate to a provable one at the lower level. 875Just as every element of the higher type should translate to at least one 876element at the lower level, 877every true statement at the higher level should translate to a true statement at the lower level. 878But this principle is violated in this case. 879\end{comment} 880Therefore such disrespectful functions cannot be lifted, and 881we must exclude them. Using \quotient{} relations 882accomplishes this exclusion. 883%Therefore we exclude such disrespectful functions 884%Ordinary function application would be intractable. 885%Therefore such disrespectful functions should be excluded 886%from relations between functions. 887%Hence a \quotient{} relation 888%cannot be fully reflexive if its domain is a function type. 889\begin{comment} 890The resulting 891%\quotient{} 892relation cannot be 893a true equivalence, 894%an equivalence, 895%an equivalence relation, 896but it could be described as an equivalence relation on the field of 897the relation, the field being the set of elements which 898are related to any element. 899\end{comment} 900 901First, we say an element $r$ {\it respects R\/} if and only if 902{\it R\/} {\it r\/} {\it r}. 903 904\begin{definition}[Quotient] 905\label{quotientdef} 906%We define that 907A relation {\it R\/} 908with 909%is a {\it \quotient{} relation\/} with respect to 910abstraction function {\it abs\/} 911and representation function {\it rep\/} 912(between the representation, lower type $\tau$ 913and the abstract, quotient type $\xi$) 914is a {\it quotient} 915(notated as $\langle R$,${\it abs}$,${\it rep} \rangle$) 916if and only if 917%the following hold: 918\end{definition} 919 920\begin{center} 921\begin{tabular}[t]{l@{\hspace{0.5cm}}l} 922%{\it rep is right inverse of abs} 923(1) 924& $\forall a:\xi.$ {\it abs} ({\it rep} $a$) = $a$ \\ 925%{\it reflexivity of rep} 926(2) 927& $\forall a:\xi.$ {\it R\/} ({\it rep} $a$) ({\it rep} $a$) \\ 928%{\it proper equivalence} 929(3) 930& $\forall r,s:\tau.$ 931{\it R\/} $r$ $s$ $\Leftrightarrow$ 932{\it R\/} $r$ $r$ $\wedge$ 933{\it R\/} $s$ $s$ $\wedge$ 934({\it abs} $r$ = {\it abs} $s$) \\ 935\end{tabular} 936\end{center} 937 938Property 1 states that {\it rep\/} is a right inverse of {\it abs}. 939 940Property 2 states that 941%{\it R\/} is reflexive on the range of {\it rep}. 942the range of {\it rep} respects {\it R}. 943 944Property 3 states that two elements of $\tau$ are related by {\it R\/} 945if and only if 946each element respects {\it R} and their abstractions are equal. 947 948%Of course, if {\it R\/} is an equivalence relation, then for example 949%it is reflexive on all elements, not only the range of {\it rep} 950%(property 2). 951%But the properties here describe a 952%{\it \quotient{} relation}, which is not the same as an equivalence relation. 953 954%These properties imply that {\it R\/} is a \quotient{} relation. 955 956These three properties (1-3) describe the way 957the \quotient{} relation {\it R\/} works together with 958{\it abs\/} and {\it rep} 959to establish the correct 960quotient relationship between the lower type $\tau$ 961and the quotient type $\xi$. 962The precise definition of this quotient relationship 963is a central contribution of this work. 964%This relationship is so important that we give it a special definition: 965This relationship is defined in the HOL logic as a new predicate: 966{\tt 967\begin{tabbing} 968\hspace{3.5mm} 969 QUOTI\=ENT (R:'a -> 'a -> bool) (abs:'a -> 'b) (rep:'b -> 'a) $\Leftrightarrow$ \\ 970\> ($\forall$a. abs (rep a) = a) $\wedge$ \\ 971\> ($\forall$a. R (rep a) (rep a)) $\wedge$ \\ 972\> ($\forall$r s. R r s $\Leftrightarrow$ R r r $\wedge$ R s s $\wedge$ (abs r = abs s)) 973\end{tabbing}} 974 975\noindent 976The relationship that {\it R\/} with {\it abs\/} and {\it rep\/} 977is a quotient is 978%concisely notated as $\langle R$,${\it abs}$,${\it rep} \rangle$, or 979expressed in HOL as 980\begin{center} 981\tt 982$\vdash$ QUOTIENT {\it R\/} {\it abs\/} {\it rep} . 983\end{center} 984 985\noindent 986A theorem of this form is called a {\it quotient theorem}. 987The identity is 988$\vdash \langle \mbox{\tt \$=}, \mbox{\tt I}, \mbox{\tt I} \rangle$. 989%They play a central role within this quotient package. 990 991\begin{comment} 992The traditional construction requires the elements of the 993%new 994quotient 995type to be subsets of the original type. 996This definition of quotients only requires them to be isomorphic. 997\end{comment} 998% 999%The above definition is a fundamental revision of the notion of quotients. 1000%As will be shown in section \ref{condquotients}, 1001These three properties support the inference of a quotient theorem for a 1002function type, given quotient theorems for the domain and the range. 1003This key inference is central and necessary to enable higher order quotients. 1004 1005 1006% 1007\section{Quotient Types} 1008% 1009\label{quotienttypes} 1010 1011The user may specify a quotient of a type $\tau$ by a relation $R$ 1012(written $\tau / R$) by giving 1013either a theorem that the relation is an equivalence relation, of the form 1014\begin{equation} 1015\vdash 1016\forall x\ y.\ R\ x\ y \ \Leftrightarrow \ (R\ x = R\ y) \ , 1017\end{equation} 1018or one 1019%by giving a theorem 1020that the relation is a nonempty partial equivalence relation, of the form 1021\begin{equation} 1022\label{PERinput} 1023\vdash 1024(\exists x.\ R\ x\ x) \ \wedge \ 1025(\forall x\ y.\ R\ x\ y \ \Leftrightarrow \ 1026 R\ x\ x \wedge R\ y\ y \wedge (R\ x = R\ y)) \ . 1027\end{equation} 1028 1029% 1030Alternatively, these theorems may be equivalently expressed as 1031$\vdash \mbox{\tt EQUIV}\ R$ or 1032$\vdash \mbox{\tt PARTIAL\_EQUIV}\ R$, respectively, 1033%These abbreviations are 1034defined in 1035%the theorems 1036{\tt EQUIV\_def} 1037and {\tt PARTIAL\_EQUIV\_def}. 1038In this section we will develop the second, more difficult case (2). 1039The first follows immediately. 1040%, where the theorem describes a nonempty partial equivalence relation. 1041In the following, $x$, $y$, $r$, $s : \tau$, $c : \tau\rightarrow{\tt bool}$, 1042and $a : \tau / R$. 1043 1044New types may be defined in HOL 1045using the function {\tt new\_type\_definition} 1046%and {\tt define\_new\_type\_bijections} 1047\cite[sections 18.2.2.3-5]{GoMe93}. 1048This function requires us to 1049%To define a new type in higher order logic, we must 1050choose a representing 1051type, and a predicate on that type denoting a subset that is nonempty. 1052 1053\begin{definition} 1054\label{quotient_type_def} 1055We define the new 1056{\it quotient type\/} $\tau / R$ 1057%\mathbin{\sim}$ 1058as isomorphic to the subset of 1059%by 1060the representing type $\tau \rightarrow \mbox{\tt bool}$ 1061%and 1062%selected 1063by the 1064predicate $P : (\tau \rightarrow \mbox{\tt bool}) \rightarrow \mbox{\tt bool}$, 1065where 1066$ 1067P \ c \ \defeq \ \exists x.\ R\ x\ x \wedge (c = R\ x). 1068$ 1069\end{definition} 1070 1071\noindent 1072{\it P\/} is nonempty because $P\ (R\ x)$ for the $x$\,:\,$\tau$ 1073such that $R\ x\ x$ by (\ref{PERinput}). 1074Let $\xi = \tau / R$. 1075The HOL tool 1076{\tt define\_new\_type\_bijections} 1077\cite{GoMe93} automatically defines 1078%in the HOL logic 1079%an abstraction 1080%function $\lceil \_ \rceil_c 1081%: (\tau \rightarrow \mbox{\tt bool}) \rightarrow \xi$ 1082%and a representation function $\lfloor \_ \rfloor_c 1083%: \xi \rightarrow (\tau \rightarrow \mbox{\tt bool}) $, such that 1084%abstraction and representation functions 1085a function 1086%$\lceil \_ \rceil_c 1087$\mbox{\it abs}_c :(\tau \rightarrow \mbox{\tt bool}) \rightarrow \xi$ 1088and its right inverse 1089%$\lfloor \_ \rfloor_c 1090$\mbox{\it rep}_c :\xi \rightarrow (\tau \rightarrow \mbox{\tt bool}) $ satisfying 1091 1092\begin{definition} 1093\label{abs_rep_classes} 1094$ 1095%(\forall a:\xi.\ \lceil \, \lfloor a \rfloor_c \rceil_c = a) 1096%\ \wedge \ 1097%(\forall f:\tau \rightarrow \mbox{\tt bool}.\ 1098%P\ f \, \Leftrightarrow (\lfloor \, \lceil f \rceil_c \rfloor_c = f)) . 1099\begin{array}[t]{ll} 1100(\mbox{\rm a})\ & \forall a:\xi.\ {\it abs}_c \ ({\it rep}_c \ a) = a 1101%\ \wedge 1102\\ 1103(\mbox{\rm b}) & \forall c:\tau \rightarrow \mbox{\tt bool}.\ 1104P\ c 1105%(\exists x.\ R\ x\ x \wedge (c = R\ x)) 1106\ \Leftrightarrow \ {\it rep}_c \ ({\it abs}_c \ c) = c 1107\end{array} 1108$ 1109\end{definition} 1110 1111\noindent 1112%{\it``PER classes''} 1113{\it PER classes\/} 1114are subsets of $\tau$ (of type $\tau \rightarrow \mbox{\tt bool}$) 1115which satisfy $P$. 1116Then ${\it abs}_c$ and ${\it rep}_c$ 1117map between 1118the quotient type $\xi$ 1119and 1120PER classes (hence the ``$c$''). 1121 1122%\noindent 1123%and returns Definition \ref{abs_rep_classes} as its result. 1124%These functions are used to create identifiable values of the new type. 1125%and to establish their interrelationships. 1126%(The `${}_c$' is notation.) 1127% 1128%For the $P$ of Definition \ref{quotient_type_def}, we can prove: 1129%\begin{theorem} 1130%\label{abs_rep_classes_simple} 1131%$ 1132%(\forall a 1133%%:\xi 1134%.\ \lceil \, \lfloor a \rfloor_c \rceil_c = a) 1135%\ \wedge \ 1136%(\forall f.\ (\exists x.\ R\ x\ x \wedge f = R\ x) \Leftrightarrow 1137%\lfloor \, \lceil \, f \rceil_c \rfloor_c = f ) . 1138%$ 1139%\end{theorem} 1140%Proof: 1141%The left conjunct comes directly from Definition \ref{abs_rep_classes}. 1142%Also by that theorem, the right conjunct is equivalent to 1143%$\forall r.\ P\ [ r ]_E$. 1144%% !r. (\c. ?r. c = ALPHA r) (ALPHA r) 1145%Then 1146%$ 1147%P\ [ r ]_E = 1148%%P\ (E\ r) = 1149%(\exists x.\ [ r ]_E = [ x ]_E) 1150%$ 1151%which is proven true by choosing the witness $x = r$. 1152%$\Box$ 1153 1154\begin{lemma}[${\it rep}_c$ maps to PER classes] 1155\label{ty_REP_REL} 1156$\forall a.\ 1157P\ ({\it rep}_c\ a)$. 1158%\exists r.\ R\ r\ r\ \wedge \ {\it rep}_c\ a = R\ r$. 1159\end{lemma} 1160Proof: 1161By 1162%the first clause of 1163Definition \ref{abs_rep_classes}(a), 1164$ {\it abs}_c\ ({\it rep}_c\ a) = a$, so taking 1165the ${\it rep}_c$ of both sides, 1166$ {\it rep}_c\ ({\it abs}_c\ ({\it rep}_c\ a)) = {\it rep}_c\ a$. 1167By 1168%the second clause of 1169Definition \ref{abs_rep_classes}(b), 1170%this implies 1171$P\ ({\it rep}_c\ a)$. 1172%By the definition of $P$, this is 1173%the goal. 1174$\Box$ 1175 1176%\begin{corollary} 1177%\label{ty_REP_REL_cor} 1178%$\forall a.\ 1179%\exists r.\ 1180%R\ r\ r\ \wedge\ {\it rep}_c\ a = R\ r$. 1181%%{\it rep}_c\ ({\it abs}_c\ ({\it rep}_c\ a)) = {\it rep}_c\ a$. 1182%\end{corollary} 1183 1184\begin{lemma} 1185\label{ty_REP_ABS} 1186$\forall r.\ 1187R\ r\ r \Rightarrow 1188({\it rep}_c\ ({\it abs}_c\ (R\ r)) = R\ r)$. 1189\end{lemma} 1190Proof: Assume $R\ r\ r$; then $P\ (R\ r)$. 1191By Definition \ref{abs_rep_classes}(b), the goal follows. 1192 1193\begin{lemma}[${\it abs}_c$ is one-to-one on PER classes] 1194\label{ty_ABS_11} 1195\\ 1196$\forall r\ s.\ 1197R\ r\ r \Rightarrow 1198R\ s\ s \Rightarrow 1199({\it abs}_c\ (R\ r) = {\it abs}_c\ (R\ s) 1200\ \Leftrightarrow \ R\ r = R\ s)$. 1201\end{lemma} 1202Proof: Assume $R\ r\ r$ and $R\ s\ s$. 1203%Then $P\ (R\ r)$ and $P\ (R\ s)$ 1204%by the definition of $P$. 1205The right-to-left implication of the biconditional is trivial. 1206Assume ${\it abs}_c\ (R\ x) = {\it abs}_c\ (R\ y)$. 1207Applying ${\it rep}_c$ to 1208both sides gives us 1209${\it rep}_c\ ({\it abs}_c\ (R\ x)) = {\it rep}_c\ ({\it abs}_c\ (R\ y))$. 1210%By Lemma \ref{ty_REP_REL}, $P$ is true of both sides. 1211%$P\ ({\it rep}_c\ ({\it abs}_c (R\ x))$. 1212Then by 1213%Definition \ref{abs_rep_classes}(b), 1214Lemma \ref{ty_REP_ABS} twice, 1215$R\ x = R\ y$. 1216$\Box$ 1217 1218\vspace{\topsep} 1219The functions 1220${\it abs}_c$ and ${\it rep}_c$ 1221map between PER classes of type 1222$\tau \rightarrow \mbox{\tt bool}$ and the quotient type $\xi$. 1223Using these functions, we can define new functions 1224${\it abs}$ and ${\it rep}$ 1225between the original 1226type $\tau$ and the quotient type $\xi$ as follows. 1227\begin{definition}[Quotient abstraction and representation functions] 1228\label{abs_rep_def} 1229$$ 1230\begin{array}[t]{c@{\hspace{0.1cm}}c@{\hspace{0.1cm}}l@{\hspace{1.0cm}}rcl} 1231{\it abs} & : & \tau \rightarrow \xi & 1232{\it abs}\ r & \ \defeq \ & 1233{\it abs}_c\ (R\ r) \\ 1234{\it rep} & : & \xi \rightarrow \tau & 1235{\it rep}\ a & \ \defeq \ & 1236\mbox{\tt \$@} \ ({\it rep}_c\ a)\ \ ( \ = \ 1237\mbox{\tt @}r.\ {\it rep}_c\ a \ r 1238%\ = \ \mbox{\tt @}x.\ ( R\ x = {\it rep}_c\ a ) 1239\ ) 1240\end{array} 1241$$ 1242\end{definition} 1243 1244The {\tt @} operator 1245%which is here used as a prefix unary operator {\tt \$@}, 1246is a higher order version of Hilbert's choice operator $\varepsilon$ 1247\cite{GoMe93,Lei69}. 1248It has type $(\alpha \rightarrow \mbox{\tt bool}) \rightarrow \alpha$, 1249%{\tt ('a -> bool) -> 'a}, 1250and is usually used as a binder, 1251where 1252%the two syntaxes are related by 1253$\mbox{\tt \$@}\ P = \mbox{\tt @}x.\ P\ x$. 1254(The {\tt \$} converts an operator to prefix syntax.) 1255%The axiom in HOL about the behavior of {\tt @} is 1256{\tt @} satisfies the HOL axiom 1257$\forall P\ x.\ P\ x \Rightarrow P\ (\mbox{\tt \$@}\ P)$. 1258Given any predicate $P$ on a type, 1259%(not confused with Definition \ref{quotient_type_def}), 1260if any element of the type satisfies the predicate, 1261then $\mbox{\tt \$@}\ P$ returns an arbitrary element of 1262that type which satisfies $P$. 1263If no element of the type satisfies $P$, 1264then $\mbox{\tt \$@}\ P$ will return simply some 1265arbitrary, 1266unknown 1267element of the type. 1268% 1269%In the definition above, {\tt @} 1270%selects some arbitrary representative $x$ such 1271%that the equivalence class of $x$ is the class representating $a$. 1272% 1273Such definitions 1274have been questioned by constructivist critics of the Axiom of Choice. 1275%are controversial. 1276An alternative design for quotients avoiding 1277%the Hilbert choice operator and 1278the Axiom of Choice 1279is described in section \ref{axiomofchoice}. 1280 1281%\begin{lemma} 1282%\label{type_exists} 1283%$\exists c.\ P\ c$ 1284%\end{lemma} 1285%Proof: Let $x$ be a value of type {\tt ty}. 1286%Then choose $c = \mbox{\it E\/}\ x$, 1287%and then $P\ c = P\ ( \mbox{\it E\/}\ x ) = 1288% (\exists r : {\tt ty}.\ {\it E\/}\ x = \mbox{\it E\/}\ r)$. 1289%Then choose $r = x$. 1290 1291\begin{lemma} 1292\label{ty_REL_SELECT_REL} 1293$\forall r.\ 1294R\ r\ r \Rightarrow 1295(R\ (\mbox{\tt \$@} \ (R\ r)) = R\ r)$. 1296\end{lemma} 1297Proof: 1298The axiom for the {\tt @} operator is 1299$\forall P\ x.\ P\ x \Rightarrow P\ (\mbox{\tt \$@}\ P)$. 1300Taking $P = R\ r$ and $x = r$, we have 1301$R\ r\ r \Rightarrow R\ r\ (\mbox{\tt \$@}\ R\ r)$. 1302Assuming $R\ r\ r$, 1303$R\ r\ (\mbox{\tt \$@} \ (R\ r))$ follows. 1304%By lemma 1305%\ref{ty_REL_SELECT} and symmetry, $R\ (\mbox{\tt \$@} \ (R\ r))\ r$. 1306Then 1307by (\ref{PERinput}), 1308%since $R\ x\ y \Leftrightarrow R\ x\ x \wedge R\ y\ y \wedge (R\ x = R\ y)$ 1309%(the partial equivalence property for $R$), 1310$R\ r\ (\mbox{\tt \$@} \ (R\ r))$ implies the equality 1311$R\ r = R\ (\mbox{\tt \$@} \ (R\ r))$. 1312$\Box$ 1313 1314\begin{theorem} 1315\label{ty_ABS_REP} 1316$\forall a.\ {\it abs}\ ({\it rep}\ a) = a$ 1317\end{theorem} 1318Proof: 1319By Lemma \ref{ty_REP_REL} 1320 and the definition of $P$, 1321%By Corollary \ref{ty_REP_REL_cor}, 1322for each $a$ 1323there exists an $r$ such that 1324$R\ r\ r$ and ${\it rep}_c\ a = R\ r$. 1325Then 1326by Lemma \ref{ty_REL_SELECT_REL}, $R\ (\mbox{\tt \$@} \ (R\ r)) = R\ r$. 1327%which is equivalent to $R\ (\mbox{\tt \$@}\ ({\it rep}_c\ a) = {\it rep}_c\ a$. 1328Now by Definition \ref{abs_rep_def}, ${\it abs}\ ({\it rep}\ a) = 1329{\it abs}_c\ (R\ (\mbox{\tt \$@}\ ({\it rep}_c\ a)))$, 1330which simplifies by the above and Definition \ref{abs_rep_classes}(a) 1331to $a$. $\Box$ 1332%equivalent to ${\it abs}_c\ ({\it rep}_c\ a)$, 1333%which by Definition \ref{abs_rep_classes} is simply $a$. 1334\begin{comment} 1335$$ 1336\begin{array}{rcl@{\hspace{2.0cm}}r} 1337{\it abs}\ ({\it rep}\ a) 1338%\lceil \, \lfloor a \rfloor \, \rceil 1339& \ = \ & 1340{\it abs}_c\ (R\ (\mbox{\tt \$@}\ ({\it rep}_c\ a))) 1341%\lceil \, [ \, \mbox{\tt \$@} \ \lfloor a {\rfloor}_c \, ]_E {\rceil}_c 1342& \mbox{Definition \ref{abs_rep_def}} \\ 1343& \ = \ & 1344{\it abs}_c\ (R\ (\mbox{\tt \$@}\ (R\ r))) 1345%\lceil \, [ \, \mbox{\tt \$@} \ [ r ]_E \, ]_E {\rceil}_c 1346& \mbox{selection of $r$} \\ 1347& \ = \ & 1348{\it abs}_c\ (R\ r) 1349& \mbox{Lemma \ref{ty_REL_SELECT_REL} and $R\ r\ r$} \\ 1350& \ = \ & 1351{\it abs}_c\ ({\it rep}_c\ a) 1352\ = \ a 1353%& \mbox{selection of $r$} \\ 1354%& \ = \ & 1355%a 1356& \mbox{selection of $r$,} \ 1357 \mbox{Definition \ref{abs_rep_classes}(a)} \\ 1358\Box \hfill & & & 1359\end{array} 1360$$ 1361\end{comment} 1362 1363\begin{theorem} 1364\label{rep_respects} 1365$\forall a.\ R\ ({\it rep}\ a)\ ({\it rep}\ a)$. 1366\end{theorem} 1367Proof: 1368As before, 1369%in Theorem \ref{ty_ABS_REP}, 1370%By Lemma \ref{ty_REP_REL} and the definition of $P$, 1371%By Corollary \ref{ty_REP_REL_cor}, 1372for each $a$ 1373there exists an $r$ such that 1374$R\ r\ r$ and ${\it rep}_c\ a = R\ r$. 1375%Then 1376%by Definition \ref{abs_rep_def}, 1377%$R\ ({\it rep}\ a)\ ({\it rep}\ a)$ 1378%is $R\ (\mbox{\tt \$@}\ ({\it rep}_c\ a))\ (\mbox{\tt \$@}\ ({\it rep}_c\ a))$, 1379%which is $R\ (\mbox{\tt \$@}\ (R\ r))\ (\mbox{\tt \$@}\ (R\ r))$, 1380%which by Lemma \ref{ty_REL_SELECT_REL} twice, 1381%using the symmetry of $R$, is $R\ r\ r$, true. 1382% 1383$$ 1384\begin{array}[t]{rcl@{\hspace{0.5cm}}r} 1385R\ (\mbox{\it rep}\ a)\ (\mbox{\it rep}\ a) 1386& \ \Leftrightarrow \ & 1387R\ (\mbox{\tt \$@}\ (\mbox{\it rep}_c\ a))\ (\mbox{\tt \$@}\ (\mbox{\it rep}_c\ a)) 1388& \mbox{Definition \ref{abs_rep_def}} \\ 1389& \ \Leftrightarrow \ & 1390R\ (\mbox{\tt \$@}\ (R\ r))\ (\mbox{\tt \$@}\ (R\ r)) 1391& \mbox{selection of $r$} \\ 1392& \ \Leftrightarrow \ & 1393R\ r\ (\mbox{\tt \$@}\ (R\ r)) 1394& \mbox{Lemma \ref{ty_REL_SELECT_REL}} \\ 1395& \ \Leftrightarrow \ & 1396R\ (\mbox{\tt \$@}\ (R\ r))\ r 1397& \mbox{symmetry of $R$} \\ 1398& \ \Leftrightarrow \ & 1399R\ r\ r \ \Leftrightarrow \ T 1400& \mbox{Lemma \ref{ty_REL_SELECT_REL}, selection of $r$} \\ 1401\Box \hfill & & & 1402\end{array} 1403$$ 1404%$\Box$ 1405 1406\begin{theorem} 1407\label{equiv_ty_ABS} 1408$\forall r\ s.\ \ R\ r\ s \ \Leftrightarrow \ 1409R\ r\ r\ \wedge \ R\ s\ s\ \wedge \ 1410({\it abs}\ r = {\it abs}\ s)$ 1411\end{theorem} 1412Proof: 1413$ 1414\begin{array}[t]{rcl@{\hspace{0.6cm}}r} 1415R\ r\ s 1416& \ \Leftrightarrow \ & 1417R\ r\ r \ \wedge\ R\ s\ s \ \wedge\ (R\ r = R\ s) 1418& \mbox{(\ref{PERinput})} \\ 1419& \ \Leftrightarrow \ & 1420R\ r\ r \ \wedge\ R\ s\ s \ \wedge\ 1421({\it abs}_c\ (R\ r) = {\it abs}_c\ (R\ s)) 1422& \mbox{Lemma \ref{ty_ABS_11}} \\ 1423%& \ \Leftrightarrow \ & 1424% \lceil E\ r {\rceil}_c = \lceil E\ s {\rceil}_c 1425%& \mbox{Definition \ref{equiv_class}} \\ 1426& \ \Leftrightarrow \ & 1427R\ r\ r \ \wedge\ R\ s\ s \ \wedge\ 1428({\it abs}\ r = {\it abs}\ s) 1429& \mbox{Definition \ref{abs_rep_def}} \\ 1430\Box \hfill & & & 1431\end{array} 1432$ 1433 1434%Because $\lfloor \_ {\rfloor}_c$ is one-to-one, 1435%$\forall a\ a'.\ (\lfloor a {\rfloor}_c = \lfloor a' {\rfloor}_c) = (a = a')$, 1436%so the goal is equivalent to 1437%$$ 1438%E\ r\ r' = 1439% (\lfloor \, \lceil r \rceil \, {\rfloor}_c = 1440% \lfloor \, \lceil r' \rceil \, {\rfloor}_c) 1441%$$ 1442%By Definition \ref{abs_rep_def}, the goal is 1443%$$ 1444%E\ r\ r' = 1445% (\lfloor \, \lceil E\ r {\rceil}_c \, {\rfloor}_c = 1446% \lfloor \, \lceil E\ r' {\rceil}_c \, {\rfloor}_c) 1447%$$ 1448%By Theorem \ref{abs_rep_classes_simple}, this simplifies to 1449%$$ 1450%E\ r\ r' = 1451% (E\ r = 1452% E\ r') 1453%$$ 1454%which is proved by Lemma \ref{ty_REL_equiv}. 1455 1456\begin{theorem} 1457\label{quotientthm} 1458$\langle R,\ {\it abs},\ {\it rep} \rangle$. 1459\end{theorem} 1460Proof: 1461By Theorems \ref{ty_ABS_REP}, 1462\ref{rep_respects}, 1463and 1464\ref{equiv_ty_ABS}, with Definition 1465\ref{quotientdef}. 1466$\Box$ 1467 1468 1469% 1470\section{Aggregate and Higher Order Quotient Theorems} 1471% 1472\label{extensions} 1473 1474Traditional quotients that lift $\tau$ to a set of $\tau$ also 1475lift lists of $\tau$ to sets of lists of $\tau$. 1476These sets are isomorphic to lists, but {\it they are not lists}. 1477In this design, when $\tau$ is lifted to $\xi$, then 1478we lift lists of $\tau$ to lists of $\xi$. 1479We preserve the type operator structure built on top of the 1480types being lifted. Similarly, we want to preserve polymorphic constants. 1481Thus we need not create a new type for each lifted version of lists, 1482but simply reuse the existing list type operator, now applied to $\xi$. 1483This preserves the type structure and enables direct use 1484of the polymorphic constants of that type operator, such as 1485{\tt HD} for lists. 1486In a theorem being lifted, we want an occurrence of 1487$\mbox{\tt HD} : \tau\ \mbox{\tt list} \rightarrow \tau$ 1488to lift to an occurrence of 1489$\mbox{\tt HD} : \xi\ \mbox{\tt list} \rightarrow \xi$. 1490%This motivated the design choice in 1491%This is vital. 1492If such a constant is not lifted to itself, the lifted version 1493of the theorem will not look like the original. 1494Hence Definition \ref{quotientdef} was 1495intentionally 1496designed 1497to preserve the vital type operator structure. 1498%so that $\tau$ could lift to any $\xi'$ isomorphic to $\xi$. 1499 1500\begin{comment} 1501\end{comment} 1502At times one wishes to not only lift a number of types across a 1503quotient operation, but also lift by extension a number of other 1504types which are dependent on the first set. For example, if we 1505lift the type of terms of the lambda calculus across alpha-equivalence, 1506then we would also expect that the types of lists or pairs involving 1507the lifted terms would follow naturally. 1508 1509In fact these do follow; one merely has to apply the type 1510operator, say {\tt list}, to the lifted type {\tt term} to produce 1511the type of lists of lifted terms {\tt (term)list}. All of the 1512theorems about lists in general now apply to lists of lifted terms, 1513and all of the theorems about lifted terms apply to the elements of 1514these lifted lists. 1515\begin{comment} 1516\end{comment} 1517 1518%However, we will see that within the {\tt define\_quotient\_types} function, 1519In the process of lifting constants and theorems, 1520quotient theorems are needed for each 1521argument and result type 1522%subtype of the type 1523of each constant being lifted. 1524%where each type involved is a subtype of the type of the constant. 1525%either the type of a parameter or the type of the result. 1526For aggregate and higher order types, 1527the tool automatically proves any needed quotient theorems 1528%for the types 1529from the available quotient theorems for the 1530constituent subtypes. 1531To accomplish this, the tool uses {\it quotient extension theorems\/} 1532(section \ref{condquotients}). 1533These are provided preproven for some standard type operators. 1534For others, 1535%new types that the user may declare, 1536new quotient extension theorems may be manually proven and then 1537included to extend the tool's power. 1538%to handle the new types. 1539\begin{comment} 1540\end{comment} 1541 1542%This section discusses the creation 1543%%and manipulation 1544%of these quotient 1545%theorems for aggregate types. 1546 1547% 1548\subsection{Aggregate and Higher Order PERs and Map Operators} 1549% 1550\label{aggregates} 1551 1552Some aggregate equivalence relation 1553operators have been already described in section \ref{equivalence}, and 1554these can equally be used to build aggregate \quotient{} relations. 1555In addition, for function types, the following is added: 1556 1557\begin{center} 1558\framebox{ 1559\begin{tabular}[t]{lrl} 1560Type & Operator \ \ \ \ \ & Type of operator \\ 1561\hline \\ 1562fun & {\tt ===> : } & {\tt ('a -> 'a -> bool) -> ('b -> 'b -> bool) ->} \\ 1563& & {\tt \ \ \ \ \ \ ('a -> 'b) -> ('a -> 'b) -> bool} \\ 1564\end{tabular} 1565} 1566\end{center} 1567 1568%\noindent 1569%The definition of the function relation operator is: 1570% 1571% related to respectfulness: 1572\begin{definition} 1573\label{funrel} 1574$(R_1\ \mbox {\tt ===>} \ R_2)\ f \ g \ \Leftrightarrow \ 1575\forall x \ y. \ R_1\ x\ y \Rightarrow R_2\ (f\ x)\ (g\ y)$. 1576\end{definition} 1577%\begin{center} 1578%{\tt (R1 ===> R2) f g \Leftrightarrow 1579% $\forall$x y. R1 x y $\Rightarrow$ R2 (f x) (g y)}. 1580%\end{center} 1581 1582Note $R_1$ {\tt ===>} $R_2$ is {\it not\/} in general an equivalence relation 1583(it is not reflexive). 1584It is reflexive at a function $f$, 1585($R_1$ {\tt ===>} $R_2$) $f$ $f$, 1586if and only if $f$ is respectful. 1587 1588% A quotient theorem relates a \quotient{} relation to abstraction 1589% and representation functions, which map between values of the original 1590% and quotient types. These abstraction and representation functions 1591% for aggregate types 1592% can be formed by particular operators, again depending on the type operator 1593% involved, using the abstraction and representation functions of the 1594% constituent subtypes of the aggregate type. 1595 1596%\begin{verbatim} 1597\begin{comment} 1598\end{comment} 1599To ease the creation of quotient theorems, 1600we provide several Standard ML functions that automatically prove the 1601necessary quotient theorems for lists, pairs, sums, options, and function types, 1602given the quotient theorems for the subtypes which are the arguments to 1603these type operators. 1604 1605\begin{center} 1606\framebox{ 1607\begin{tabular}[t]{rl} 1608{\tt list\_quotient} & {\tt : thm -> thm} \\ 1609{\tt pair\_quotient} & {\tt : thm -> thm -> thm} \\ 1610{\tt sum\_quotient} & {\tt : thm -> thm -> thm} \\ 1611{\tt option\_quotient} & {\tt : thm -> thm} \\ 1612{\tt fun\_quotient} & {\tt : thm -> thm -> thm} \\ 1613\\ 1614{\tt identity\_quotient} & {\tt : hol\_type -> thm} \\ 1615{\tt make\_quotient} & {\tt : thm list -> hol\_type -> thm} \\ 1616\end{tabular} 1617} 1618\end{center} 1619 1620These functions prove and return quotient theorems, 1621of the form 1622\begin{center} 1623$\vdash$ {\tt QUOTIENT} {\it R\/} {\it abs\/} {\it rep} 1624\end{center} 1625%created by 1626%as that returned by the function {\tt define\_quotient\_type} 1627%(see the bottom of page 4). 1628% 1629%These functions do not create new types, since the types are formed 1630%using the existing {\tt list}, {\tt prod}, {\tt sum}, {\tt option}, 1631%and {\tt fun} type operators. 1632The first five functions all take as arguments quotient theorems 1633for the constituent subtypes that are arguments 1634to the aggregate type operator. The last two take an {\tt hol\_type} as 1635an argument, which is the type of elements compared by the \quotient{} relation 1636of the desired quotient theorem. 1637None of these create any new types, 1638they simply apply existing type operators. 1639 1640Sometimes one desires to perform the quotient operation on some 1641arguments of the type operator but not on others. In these 1642cases, to indicate an argument which is not to be changed, 1643supply in that place 1644a quotient theorem 1645%may be 1646created by the 1647{\tt identity\_quotient} function, which takes any HOL type and 1648returns the identity quotient theorem for that type, 1649using equality and the identity function, 1650%using simple equality ({\tt =}) and the identity function {\tt I}, 1651%where the \quotient{} relation 1652%used in the quotient theorem is simple equality ({\tt =}) 1653%between items of that type. 1654 1655\begin{center} 1656{\tt $\vdash$ QUOTIENT (\$= : ty -> ty -> bool) (I: ty -> ty) (I: ty -> ty)} 1657\end{center} 1658 1659In case one would need to create a quotient theorem for a complex type, 1660the {\tt make\_quotient} function takes a list of 1661%base (not aggregate) 1662quotient theorems and an HOL type, and returns a quotient theorem for 1663that type, automatically constructing it recursively 1664according to the structure of the type 1665and the supplied quotient theorems. 1666% for the bases. 1667\begin{comment} 1668\end{comment} 1669%\end{verbatim} 1670 1671%(* Type Operator Constructor Abstraction Equivalence *) 1672%(* *) 1673%(* Identity I x I $= *) 1674%(* Product (ty1 # ty2) (a,b) (abs1 ## abs2) (R1 ### R2) *) 1675%(* Sum (ty1 + ty2) (INL x) (abs1 ++ abs2) (R1 +++ R2) *) 1676%(* List (ty list) (CONS h t) (MAP abs) (LIST_REL R) *) 1677%(* Option (ty option) (SOME x) (OPTION_MAP abs) (OPTION_REL R) *) 1678%(* Function (ty1 -> ty2) (\x. f x) (rep1 --> abs2) (rep1 =-> abs2) *) 1679%(* (Strong respect) (R1 ===> R2) *) 1680 1681The quotient theorems 1682created for aggregate types 1683%returned by the aggregate quotient functions 1684involve not only aggregate \quotient{} relations, but also 1685aggregate abstraction and representation functions. These are constructed 1686from the component abstraction and representation functions using the 1687following ``map'' operators. 1688 1689\begin{center} 1690\framebox{ 1691\begin{tabular}[t]{lrl} 1692Type & Operator \ \ \ \ \ & Type of operator, examples of {\it abs\/} and 1693{\it rep\/} fns \\ 1694\hline \\ 1695list & {\tt MAP : } & {\tt ('a -> 'b) -> 'a list -> 'b list} \\ 1696& & \hspace{3mm} {\it examples:} ({\tt MAP} {\it abs}) , ({\tt MAP} {\it rep}) \\ 1697\\ 1698pair & {\tt \#\# : } & {\tt ('a -> 'b) -> ('c -> 'd) ->} \\ 1699& & {\tt \ \ \ \ 'a \# 'c -> 'b \# 'd} \\ 1700& & \hspace{3mm} {\it examples:} (${\it abs}_1$ {\tt \#\#} ${\it abs}_2$) , 1701 (${\it rep}_1$ {\tt \#\#} ${\it rep}_2$) \\ 1702\\ 1703sum & {\tt ++ : } & {\tt ('a -> 'b) -> ('c -> 'd) ->} \\ 1704& & {\tt \ \ \ \ 'a + 'c -> 'b + 'd} \\ 1705& & \hspace{3mm} {\it examples:} (${\it abs}_1$ {\tt ++} ${\it abs}_2$) , 1706 (${\it rep}_1$ {\tt ++} ${\it rep}_2$) \\ 1707\\ 1708option\ \ & {\tt OPTION\_MAP : } & {\tt ('a -> 'b) -> 'a option -> 'b option} \\ 1709& & \hspace{3mm} {\it examples:} ({\tt OPTION\_MAP} ${\it abs}$) , 1710 ({\tt OPTION\_MAP} ${\it rep}$) \\ 1711\\ 1712fun & {\tt --> : } & {\tt ('a -> 'b) -> ('c -> 'd) ->} \\ 1713& & {\tt \ \ \ \ ('b -> 'c) -> 'a -> 'd} \\ 1714& & \hspace{3mm} {\it examples:} (${\it rep}_1$ {\tt -->} ${\it abs}_2$) , 1715 (${\it abs}_1$ {\tt -->} ${\it rep}_2$) \\ 1716% & & \hspace{3mm} {\it definition:} 1717% {\tt (f --> g) h x = g (h (f x))} \\ 1718\end{tabular} 1719} 1720\end{center} 1721 1722\noindent 1723The definitions of the above operators are indicated below. 1724They are created either in the quotient package or in standard HOL. 1725 1726\begin{definition} 1727\label{listmap} 1728$\begin{array}[t]{lccl} 1729\mbox{\tt MAP}\ f & \mbox{\tt []} & \ = \ & \mbox{\tt []} \\ 1730\mbox{\tt MAP}\ f & (a \mbox{\tt ::} as) & \ = \ 1731 & (f\ a)\ \mbox{\tt ::}\ (\mbox{\tt MAP}\ f\ as) 1732\end{array}$ 1733\end{definition} 1734 1735\begin{definition} 1736\label{pairmap} 1737$\begin{array}[t]{lccl} 1738(f_1\ \mbox{\tt \#\#}\ f_2) & (a_1, \ a_2) & \ = \ 1739 & (f_1\ a_1, \ f_2\ a_2) 1740\end{array}$ 1741\end{definition} 1742 1743\begin{definition} 1744\label{summap} 1745$\begin{array}[t]{lccl} 1746(f_1\ \mbox{\tt ++}\ f_2) & (\mbox{\tt INL}\ a_1) & \ = \ 1747 & \mbox{\tt INL}\ (f_1\ a_1) \\ 1748(f_1\ \mbox{\tt ++}\ f_2) & (\mbox{\tt INR}\ a_2) & \ = \ 1749 & \mbox{\tt INR}\ (f_2\ a_2) 1750\end{array}$ 1751\end{definition} 1752 1753\begin{definition} 1754\label{optionmap} 1755$\begin{array}[t]{lccl} 1756\mbox{\tt OPTION\_MAP}\ f & \mbox{\tt NONE} & \ = \ 1757 & \mbox{\tt NONE} \\ 1758\mbox{\tt OPTION\_MAP}\ f & (\mbox{\tt SOME}\ a) & \ = \ 1759 & \mbox{\tt SOME}\ (f\ a) 1760\end{array}$ 1761\end{definition} 1762 1763The 1764%definition of the 1765function map operator definition is of special interest: 1766 1767\begin{definition} 1768\label{funmap} 1769$(f\ \mbox{\tt -->}\ g)\ h\ x \ \defeq \ 1770g\ (h\ (f\ x))$. 1771\end{definition} 1772%\begin{center} 1773%{\tt (f --> g) h x = g (h (f x))}. 1774%%{\tt f --> g = ($\lambda$h x. g (h (f x)))}. 1775%\end{center} 1776 1777\noindent 1778{\tt MAP} and {\tt OPTION\_MAP} are prefix operators, 1779and the others are infix. 1780The identity quotient map operator is the identity operator 1781$\mbox{\tt I}:\alpha \rightarrow \alpha$. 1782%$\mbox{\tt I:'a} \rightarrow \mbox{\tt 'a}$. 1783 1784These map operators are inserted automatically 1785in the quotient theorems created 1786for extended types. 1787%by the extended quotient functions. 1788Each resulting quotient theorem establishes that the extended type's 1789\quotient{} relation, 1790abstraction function, and representation function properly relate together 1791to form a quotient of the 1792%appropriate 1793extended type. 1794 1795%The map operator definitions 1796%may be needed to prove 1797%the preservation 1798%%``definitions'' 1799%of new polymorphic operators (see 1800%section \ref{polypreserves}). 1801 1802% 1803\subsection{Quotient Extension Theorems} 1804% 1805\label{condquotients} 1806 1807%%The 1808%%%{\tt define\_quotient\_types} and 1809%%{\tt make\_quotient} 1810%%function supports the extension of quotients 1811%%over any type operator for which a quotient extension theorem is 1812%%included in the first argument of {\tt make\_quotient}. 1813%%the list of theorems. 1814%A quotient extension theorem 1815%has antecedents 1816%%which are statements 1817%that the constituent subtypes 1818%of the type operator are quotients, and a consequent that states that the 1819%extension over the type operator is a quotient. 1820%Each antecedent has the form of a quotient theorem, but the types involved 1821%are simple type variables in the HOL logic. 1822%\begin{center} 1823%\begin{tabular}{rl} 1824%{\tt |-} 1825%& {\tt $\forall$R1 (abs1:$\alpha_1$->$\beta_1$) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ ...} \\ 1826%%& {\tt ...} \\ 1827%& {\tt $\forall$Rn (absn:$\alpha_n$->$\beta_n$) repn. QUOTIENT Rn absn repn $\Rightarrow$} \\ 1828%& {\tt QUOTIENT (OP\_REL R1 ... Rn) (OP\_MAP abs1 ... absn rep1 ... repn)} \\ 1829%& 1830%%\hspace{50mm} 1831%\hfill 1832%{\tt (OP\_MAP rep1 ... repn abs1 ... absn)} 1833%\end{tabular} 1834%\end{center} 1835% 1836%\noindent 1837%%where 1838%{\tt OP\_REL} creates a \quotient{} relation for the type operator 1839%$(\alpha_1,...,\alpha_n)op$. 1840%%as described in section \ref{equivalence} 1841%%or earlier in this section for the operator {\tt ===>} for function types, 1842%%and 1843%%where 1844%{\tt OP\_MAP} is a map operator which takes up to $2n$ arguments, 1845%%which are 1846%taken from 1847%%all 1848%%either 1849%the 1850%abstraction and representation functions 1851%between the types $\alpha_1$ through $\alpha_n$ 1852%and $\beta_1$ through $\beta_n$. 1853%%respectively, 1854%%and, 1855%Depending on the order of the arguments, it 1856%yields either an abstraction or representation function 1857%between 1858%%the types 1859%$(\alpha_1,...,\alpha_n)op$ 1860%and $(\beta_1,...,\beta_n)op$. 1861 1862Here are the quotient extension theorems for the {\tt list}, {\tt prod}, 1863{\tt sum}, {\tt option}, and, most significantly, {\tt fun} type operators: 1864 1865{\tt \begin{tabbing} 1866LIS\=T\_QUOTIENT: \\ 1867\> $\vdash$ \=$\forall R\;$\=${\it abs}\;{\it rep}.\ 1868 \langle R,{\it abs},{\it rep} \rangle \Rightarrow 1869 \langle \mbox{\tt LIST\_REL}\;R,\ 1870 \mbox{\tt MAP}\;{\it abs},\ \mbox{\tt MAP}\;{\it rep} \rangle$ \\ 1871%\> $\vdash$ \=$\forall$R\= \ abs rep. QUOTIENT R abs rep $\Rightarrow$ \\ 1872%\>\>\> QUOTIENT (LIST\_REL R) (MAP abs) (MAP rep) \\ 1873\\ 1874PAIR\_QUOTIENT: \\ 1875\> $\vdash$ $\forall R_1\;{\it abs}_1\;{\it rep}_1.\ 1876 \langle R_1,{\it abs}_1,{\it rep}_1 \rangle \Rightarrow \ 1877 \forall R_2\;{\it abs}_2\;{\it rep}_2.\ 1878 \langle R_2,{\it abs}_2,{\it rep}_2 \rangle \Rightarrow $ \\ 1879\>\>\> $\langle R_1\;\mbox{\tt \#\#\#}\;R_2,\ 1880 {\it abs}_1\;\mbox{\tt \#\#}\;{\it abs}_2,\ 1881 {\it rep}_1\;\mbox{\tt \#\#}\;{\it rep}_2 1882 \rangle$ \\ 1883%\> $\vdash$ $\forall$R1 abs1 rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\ 1884%\>\> $\forall$R2 abs2 rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\ 1885%\>\>\> QUOTIENT (R1 \#\#\# R2) (abs1 \#\# abs2) (rep1 \#\# rep2) \\ 1886\\ 1887SUM\_QUOTIENT: \\ 1888\> $\vdash$ $\forall R_1\;{\it abs}_1\;{\it rep}_1.\ 1889 \langle R_1,{\it abs}_1,{\it rep}_1 \rangle \Rightarrow \ 1890 \forall R_2\;{\it abs}_2\;{\it rep}_2.\ 1891 \langle R_2,{\it abs}_2,{\it rep}_2 \rangle \Rightarrow $ \\ 1892\>\>\> $\langle R_1\;\mbox{\tt +++}\;R_2,\ 1893 {\it abs}_1\;\mbox{\tt ++}\;{\it abs}_2,\ 1894 {\it rep}_1\;\mbox{\tt ++}\;{\it rep}_2 1895 \rangle$ \\ 1896%\> $\vdash$ $\forall$R1 abs1 rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\ 1897%\>\> $\forall$R2 abs2 rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\ 1898%\>\>\> QUOTIENT (R1 +++ R2) (abs1 ++ abs2) (rep1 ++ rep2) \\ 1899\\ 1900OPTION\_QUOTIENT: \\ 1901\> $\vdash$ $\forall R\;{\it abs}\;{\it rep}.\ 1902 \langle R,{\it abs},{\it rep} \rangle \Rightarrow $ \\ 1903\>\>\> $\langle \mbox{\tt OPTION\_REL}\;R,\ 1904 \mbox{\tt OPTION\_MAP}\;{\it abs},\ \mbox{\tt OPTION\_MAP}\;{\it rep} \rangle$ \\ 1905%\> $\vdash$ $\forall$R abs rep. QUOTIENT R abs rep $\Rightarrow$ \\ 1906%\>\>\> QUOTIENT (OPTION\_REL R) (OPTION\_MAP abs) (OPTION\_MAP rep) \\ 1907\\ 1908FUN\_QUOTIENT: \\ 1909\> $\vdash$ $\forall R_1\;{\it abs}_1\;{\it rep}_1.\ 1910 \langle R_1,{\it abs}_1,{\it rep}_1 \rangle \Rightarrow \ 1911 \forall R_2\;{\it abs}_2\;{\it rep}_2.\ 1912 \langle R_2,{\it abs}_2,{\it rep}_2 \rangle \Rightarrow $ \\ 1913\>\>\> $\langle R_1\;\mbox{\tt ===>}\;R_2,\ 1914 {\it rep}_1\;\mbox{\tt -->}\;{\it abs}_2,\ 1915 {\it abs}_1\;\mbox{\tt -->}\;{\it rep}_2 1916 \rangle$ 1917%\> $\vdash$ $\forall$R1 abs1 rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\ 1918%\>\> $\forall$R2 abs2 rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\ 1919%\>\>\> QUOTIENT (R1 ===> R2) (rep1 --> abs2) (abs1 --> rep2) 1920\end{tabbing}} 1921 1922This last theorem is of central and critical importance to forming higher order 1923quotients. 1924We present here its proof in detail. 1925 1926\begin{theorem}[Function quotients] 1927\label{funquotient} 1928If relations $R_1$ and $R_2$ 1929with 1930%are \quotient{} relations with respect to 1931abstraction functions ${\it abs}_1$ and ${\it abs}_2$ 1932and representation functions ${\it rep}_1$ and ${\it rep}_2$, 1933respectively, 1934are quotients, 1935then $R_1$ {\tt ===>} $R_2$ 1936with 1937%is a \quotient{} relation with respect to 1938abstraction function ${\it rep}_1$ {\tt -->} ${\it abs}_2$ 1939and representation function 1940${\it abs}_1$~{\tt -->}~${\it rep}_2$ 1941is a quotient. 1942 1943%If $R_1$ and $R_2$ are \quotient{} 1944%relations with respect to 1945%abstraction functions ${\it abs}_1$ and ${\it abs}_2$ 1946%and representation functions ${\it rep}_1$ and ${\it rep}_2$, 1947%respectively, 1948%then $R_1$ {\tt ===>} $R_2$ is a \quotient{} relation with 1949%respect to 1950%abstraction function ${\it rep}_1$ {\tt -->} ${\it abs}_2$ 1951%and representation function 1952%${\it abs}_1$~{\tt -->}~${\it rep}_2$. 1953\end{theorem} 1954{\bf Proof:} 1955We need to prove the three properties of 1956Definition \ref{quotientdef}: 1957%in section \ref{quotientrelation}: 1958% for $R_1$ {\tt ===>} $R_2$ to be a \quotient{} relation with 1959%respect to 1960% abstraction function ${\it rep}_1$ {\tt -->} ${\it abs}_2$ 1961% and representation function ${\it abs}_1$ {\tt -->} ${\it rep}_2$: 1962 1963{\it Property 1.} Prove for all $a$, 1964(${\it rep}_1$ {\tt -->} ${\it abs}_2$) 1965((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$) = $a$. \\ 1966Proof: 1967The equality here is between functions, and by extension, true if 1968for all values $x$ in $a$'s domain, 1969(${\it rep}_1$ {\tt -->} ${\it abs}_2$) 1970((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$) $x$ = $a$ $x$. \\ 1971By the definition of {\tt -->}, this is 1972${\it abs}_2$ 1973((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$ (${\it rep}_1$ $x$)) = $a$ $x$, 1974and then 1975${\it abs}_2$ (${\it rep}_2$ ($a$ (${\it abs}_1$ (${\it rep}_1$ $x$)))) = $a$ $x$. 1976By Property 1 of $\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$, 1977${\it abs}_1$ (${\it rep}_1$ $x$) = $x$, and 1978by Property 1 of $\langle R_2$,${\it abs}_2$,${\it rep}_2 \rangle$, 1979$\forall b.\ {\it abs}_2$ (${\it rep}_2$ $b$) = $b$, so 1980this reduces to $a$ $x$ = $a$ $x$, true. 1981 1982{\it Property 2.} Prove 1983($R_1$ {\tt ===>} $R_2$) 1984((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$) 1985((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$). \\ 1986Proof: 1987By the definition of {\tt ===>}, this is \\ 1988$\forall x, y.$ 1989$R_1 \ x \ y \ \Rightarrow$ $R_2$ 1990((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$ $x$) 1991((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$ $y$). 1992Assume $R_1 \ x \ y$, and show $R_2$ 1993((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$ $x$) 1994((${\it abs}_1$ {\tt -->} ${\it rep}_2$) $a$ $y$). 1995By the definition of {\tt -->}, this is $R_2$ 1996(${\it rep}_2$ ($a$ (${\it abs}_1$ $x$))) 1997(${\it rep}_2$ ($a$ (${\it abs}_1$ $y$))). 1998Now since $R_1 \ x \ y$, by Property 3 of $\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$, 1999${\it abs}_1$ $x$ = ${\it abs}_1$ $y$. 2000Substituting this into our goal, we must prove $R_2$ 2001(${\it rep}_2$ ($a$ (${\it abs}_1$ $y$))) 2002(${\it rep}_2$ ($a$ (${\it abs}_1$ $y$))). 2003But this is an instance of Property 2 of 2004$\langle R_2$,${\it abs}_2$,${\it rep}_2 \rangle$, and 2005so the goal is proven. 2006 2007{\it Property 3.} Prove 2008($R_1$ {\tt ===>} $R_2$) $r$ $s$ $\Leftrightarrow$ 2009%{\it (if and only if)} 2010\\ 2011($R_1$ {\tt ===>} $R_2$) $r$ $r$ $\wedge$ 2012($R_1$ {\tt ===>} $R_2$) $s$ $s$ 2013%\hspace*{\fill} 2014$\wedge$ 2015((${\it rep}_1$ {\tt -->} ${\it abs}_2$) $r$ = 2016(${\it rep}_1$ {\tt -->} ${\it abs}_2$) $s$). \\ 2017The last conjunct on the right side is equality between functions, so by extension this is 2018($R_1$ {\tt ===>} $R_2$) $r$ $s$ $\Leftrightarrow$ 2019($R_1$ {\tt ===>} $R_2$) $r$ $r$ $\wedge$ 2020($R_1$ {\tt ===>} $R_2$) $s$ $s$ $\wedge$ \\ 2021\hspace*{\fill} 2022($\forall x.$ (${\it rep}_1$ {\tt -->} ${\it abs}_2$) $r$ $x$ = 2023 (${\it rep}_1$ {\tt -->} ${\it abs}_2$) $s$ $x$). \\ 2024By the definitions of {\tt ===>} and {\tt -->}, this is 2025$(1) \Leftrightarrow (2) \wedge (3) \wedge (4)$, where 2026\begin{center} 2027\begin{tabular}{r@{\hspace{10mm}}l} 2028(1) & 2029($\forall x\ y.\ R_1 \ x \ y \ \Rightarrow$ $R_2$ ($r$ $x$) ($s$ $y$)) 2030 \\ 2031(2) & 2032($\forall x\ y.\ R_1 \ x \ y \ \Rightarrow$ $R_2$ ($r$ $x$) ($r$ $y$)) 2033\\ 2034(3) & 2035($\forall x\ y.\ R_1 \ x \ y \ \Rightarrow$ $R_2$ ($s$ $x$) ($s$ $y$)) 2036\\ 2037(4) & 2038($\forall x.$ (${\it abs}_2$ ($r$ (${\it rep}_1$ $x$)) = 2039 ${\it abs}_2$ ($s$ (${\it rep}_1$ $x$))). \\ 2040\end{tabular} 2041\end{center} 2042We prove 2043$(1) \Leftrightarrow (2) \wedge (3) \wedge (4)$ 2044as a biconditional with two goals. 2045% 2046%\begin{center} 2047%\begin{tabular}{r@{\hspace{10mm}}l} 2048%(1) & 2049%($\forall x,y.\ R_1 \ x \ y \ \Rightarrow$ $R_2$ ($r$ $x$) ($s$ $y$)) 2050%= \\ 2051%(2) & 2052%\hspace{3mm} 2053%($\forall x,y.\ R_1 \ x \ y \ \Rightarrow$ $R_2$ ($r$ $x$) ($r$ $y$)) 2054%$\wedge$ \\ 2055%(3) & 2056%\hspace{3mm} 2057%($\forall x,y.\ R_1 \ x \ y \ \Rightarrow$ $R_2$ ($s$ $x$) ($s$ $y$)) 2058%$\wedge$ \\ 2059%(4) & 2060%\hspace{3mm} 2061%($\forall x.$ (${\it abs}_2$ ($r$ (${\it rep}_1$ $x$)) = 2062% ${\it abs}_2$ ($s$ (${\it rep}_1$ $x$))). \\ 2063%\end{tabular} 2064%\end{center} 2065% (1) ($\forall$x y. R1 x y $\Rightarrow$ R2 (r x) (s y)) = 2066% (2) ($\forall$x y. R1 x y $\Rightarrow$ R2 (r x) (r y)) /\ 2067% (3) ($\forall$x y. R1 x y $\Rightarrow$ R2 (s x) (s y)) /\ 2068% (4) $\forall$x. abs2 (r (rep1 x)) = abs2 (s (rep1 x)) 2069%The equality at the end of the first line is between booleans. 2070%We prove this as a biconditional with two goals. 2071 2072{\it Goal 1.} 2073($\Rightarrow$) 2074Assume (1). Then we must prove (2), (3), and (4). 2075 2076{\it Subgoal 1.1.} (Proof of (2)) 2077Assume $R_1$ $x$ $y$. We must prove $R_2$ ($r$ $x$) ($r$ $y$). 2078From $R_1$ $x$ $y$ and Property 3 of 2079$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$, 2080we also have 2081$R_1$ $x$ $x$ and 2082$R_1$ $y$ $y$. 2083From (1) and $R_1$ $x$ $y$, we have $R_2$ ($r$ $x$) ($s$ $y$). 2084From (1) and $R_1$ $y$ $y$, we have $R_2$ ($r$ $y$) ($s$ $y$). 2085Then by symmetry and transitivity of $R_2$, the goal is proven. 2086 2087{\it Subgoal 1.2.} (Proof of (3)) Similar to the previous subgoal. 2088 2089{\it Subgoal 1.3.} (Proof of (4)) 2090%Show 2091% ${\it abs}_2$ ($r$ (${\it rep}_1$ $x$)) = 2092% ${\it abs}_2$ ($s$ (${\it rep}_1$ $x$)). 2093$R_1$ (${\it rep}_1$ $x$) (${\it rep}_1$ $x$) follows from 2094Property 2 of 2095$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$. 2096From (1), 2097we have 2098$R_2$ ($r$ (${\it rep}_1$ $x$)) ($s$ (${\it rep}_1$ $x$)). 2099Then the goal follows from this and the third conjunct of Property 3 of 2100$\langle R_2$,${\it abs}_2$,${\it rep}_2 \rangle$. 2101 2102{\it Goal 2.} ($\Leftarrow$) 2103Assume (2), (3), and (4). We must prove (1). 2104Assume $R_1\ x\ y$. Then we must prove $R_2$ ($r$ $x$) ($s$ $y$). 2105From $R_1\,x\ y$ and Property 3 of 2106$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$, 2107we also have 2108$R_1\,x\ x$, 2109$R_1\,y\ y$, and 2110${\it abs}_1$ $x$ = ${\it abs}_1$ $y$. 2111By Property 3 of 2112$\langle R_2$,${\it abs}_2$,${\it rep}_2 \rangle$, 2113the goal is 2114$R_2$ ($r$ $x$) ($r$ $x$) $\wedge$ 2115$R_2$ ($s$ $y$) ($s$ $y$) $\wedge$ 2116${\it abs}_2$ ($r$ $x$) = ${\it abs}_2$ ($s$ $y$). 2117This breaks into three subgoals. 2118 2119{\it Subgoal 2.1.} Prove $R_2$ ($r$ $x$) ($r$ $x$). 2120This follows from 2121$R_1$ $x$ $x$ and (2). 2122 2123{\it Subgoal 2.2.} Prove $R_2$ ($s$ $y$) ($s$ $y$). 2124This follows from 2125$R_1$ $y$ $y$ and (3). 2126 2127\pagebreak[3] 2128{\it Subgoal 2.3.} Prove ${\it abs}_2$ ($r$ $x$) = ${\it abs}_2$ ($s$ $y$). 2129%\begin{lemma} 2130\begin{center} 2131\begin{minipage}{3.8in} 2132%\addtolength{\leftmargin}{1.0cm} 2133{\bf Lemma.} {\it 2134If 2135$\langle R$,${\it abs}$,${\it rep} \rangle$ 2136and 2137$R$ $z$ $z$, then {\rm $R$ (${\it rep}$ (${\it abs}$ $z$)) $z$}. 2138%\end{lemma} 2139} \\ 2140$R$ (${\it rep}$ (${\it abs}$ $z$)) (${\it rep}$ (${\it abs}$ $z$)), 2141by Property 2 of 2142$\langle R$,${\it abs}$,${\it rep} \rangle$. 2143%We already have 2144From the hypothesis, 2145$R$ $z$ $z$. 2146From Property 1 of 2147$\langle R$,${\it abs}$,${\it rep} \rangle$, 2148\linebreak[3] 2149${\it abs}$~(${\it rep}$ (${\it abs}$ $z$)) = ${\it abs}$ $z$. 2150From these three statements and Property 3 of 2151$\langle R$,${\it abs}$,${\it rep} \rangle$, 2152we have 2153$R$~(${\it rep}$ (${\it abs}$ $z$)) $z$. 2154%If 2155%$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$ 2156%and 2157%$R_1$ $z$ $z$, then {\rm $R_1$ (${\it rep}_1$ (${\it abs}_1$ $z$)) $z$}. 2158%%\end{lemma} 2159%} \\ 2160%$R_1$ (${\it rep}_1$ (${\it abs}_1$ $z$)) (${\it rep}_1$ (${\it abs}_1$ $z$)), 2161%by Property 2 of 2162%$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$. 2163%%We already have 2164%From the hypothesis, 2165%$R_1$ $z$ $z$. 2166%From Property 1 of 2167%$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$, 2168%\linebreak[3] 2169%${\it abs}_1$~(${\it rep}_1$ (${\it abs}_1$ $z$)) = ${\it abs}_1$ $z$. 2170%From these three statements and Property 3 of 2171%$\langle R_1$,${\it abs}_1$,${\it rep}_1 \rangle$, 2172%we have 2173%$R_1$~(${\it rep}_1$ (${\it abs}_1$ $z$)) $z$. 2174% 2175$\Box$ 2176\end{minipage} 2177\end{center} 2178%\addtolength{\leftmargin}{-1.0cm} 2179 2180By the lemma and $R_1$ $x$ $x$, we have 2181$R_1$~(${\it rep}_1$ (${\it abs}_1$ $x$)) $x$. 2182Similarly, 2183by the lemma and $R_1$ $y$ $y$, we have 2184$R_1$~(${\it rep}_1$ (${\it abs}_1$ $y$)) $y$. 2185Then by (2), we have 2186\linebreak[3] 2187$R_2$~($r$ (${\it rep}_1$ (${\it abs}_1$ $x$))) ($r$ $x$), and 2188by (3), 2189$R_2$~($s$~(${\it rep}_1$ (${\it abs}_1$ $y$))) ($s$ $y$). 2190From these and Property 3 of 2191$\langle R_2$,${\it abs}_2$,${\it rep}_2 \rangle$, 2192\begin{center} 2193\begin{tabular}{rcl} 2194${\it abs}_2$ ($r$ (${\it rep}_1$ (${\it abs}_1$ $x$))) 2195& = & ${\it abs}_2$ ($r$ $x$) 2196and \\ 2197${\it abs}_2$ ($s$ (${\it rep}_1$ (${\it abs}_1$ $y$))) 2198& = & ${\it abs}_2$ ($s$ $y$). 2199\end{tabular} 2200\end{center} 2201But by ${\it abs}_1$ $x$ = ${\it abs}_1$ $y$ and (4), 2202the left hand sides of these two equations are equal, so 2203their right hand sides must be also, 2204${\it abs}_2$ ($r$ $x$) = ${\it abs}_2$ ($s$ $y$), which proves the goal. 2205$\Box$ 2206 2207 2208% 2209\section{The Axiom of Choice} 2210% 2211\label{axiomofchoice} 2212 2213Gregory Moore wrote that ``Rarely have the practitioners of mathematics, 2214a discipline known for the certainty of its conclusions, differed so vehemently 2215over one of its central premises as they have done over the Axiom of Choice. 2216Yet without the Axiom, mathematics today would be quite different'' 2217\cite{Moore82}. 2218Today, 2219%a hundred years after Zermelo formulated the Axiom of Choice in 1904, 2220this discussion continues. 2221%in particular within the field of mechanical theorem proving. 2222Some theorem provers are based on classical logic, 2223and others on 2224%while others choose 2225%the restrictions of 2226a constructivist logic. 2227In higher order logic, the Axiom of Choice is represented 2228by Hilbert's $\varepsilon$-operator \cite[\S4.4]{Lei69}, 2229also called the indefinite description 2230operator. 2231%\cite[\S 5.10]{NiPaWe02}. 2232 Paulson's lucid recent work \cite{LP04} exhibits an approach to quotients 2233which avoids the use of Hilbert's $\varepsilon$-operator, 2234by 2235instead 2236using the definite description operator~$\iota$ 2237\cite[\S 5.10]{NiPaWe02}. 2238%\cite[ch.IV \S 4.1]{Lei69} 2239These two operators may be axiomatized as follows: 2240%\begin{eqnarray*} 2241%& \forall P\ x.\ P\ x \Rightarrow P (\varepsilon \ P) & 2242%\\ 2243%& \forall P\ x.\ P\ x \Rightarrow (\forall y.\ P\ y \Rightarrow x = y) \Rightarrow P (\iota \ P) & 2244%\end{eqnarray*} 2245%or equivalently, in a manner which shows their similarity, 2246%\begin{eqnarray*} 2247%& \forall P.\ (\exists x.\ P\ x) \Rightarrow P (\varepsilon \ P) & 2248%\\ 2249%& \forall P.\ (\exists ! x.\ P\ x) \Rightarrow P (\iota \ P) & 2250%\end{eqnarray*} 2251% 2252$$\begin{array}{cp{3mm}cp{3mm}c} 2253\forall P\ x.\ P\ x \Rightarrow P (\varepsilon \ P) & & or & & 2254\forall P.\ (\exists x.\ P\ x) \Rightarrow P (\varepsilon \ P) 2255\\ 2256\forall P\ x.\ P\ x \Rightarrow (\forall y.\ P\ y \Rightarrow x = y) \Rightarrow P (\iota \ P) & & or & & 2257\forall P.\ (\exists ! x.\ P\ x) \Rightarrow P (\iota \ P) 2258\end{array} 2259$$ 2260 2261\noindent 2262The $\iota$-operator yields the single element of a singleton set, 2263$\iota \{z\} = z$, but its result on non-singleton sets is indeterminate. 2264By contrast, the $\varepsilon$-operator chooses some 2265indeterminate 2266element of any non-empty set, even if nondenumerable. 2267%where the particular element chosen is indeterminate. 2268% 2269%The $\varepsilon$-operator is weaker than the Axiom of Choice, as 2270%Leisenring states that ``it does not necessarily follow that the axiom 2271%of choice is derivable in a formulization of set theory 2272%which is based on the $\varepsilon$-calculus'' \cite{Lei69}. 2273%Nevertheless, 2274The $\iota$-operator is 2275%strictly 2276weaker than the $\varepsilon$-operator, 2277and less objectionable to constructivists. 2278%The Hilbert $\varepsilon$-operator 2279%expresses the description of an object whose existence 2280%is known without giving a method for constructing it or identifying 2281%exactly which object is chosen, which 2282%are key features of the Axiom of Choice. 2283 2284Thus it is of interest to determine if a design for higher order quotients 2285may be formulated using only $\iota$, not $\varepsilon$. 2286Inspired by 2287%Paulson's work, 2288%Following 2289Paulson, 2290we 2291investigate this 2292by forming an alternative design, 2293eliminating the representation functions. 2294%redefine quotients. 2295%Inspired by Paulson's work, 2296%we can redefine 2297% the definition of 2298%quotients as follows. 2299 2300\begin{definition}[Constructive quotient, replacing Definition \ref{quotientdef}] 2301\label{quotientdef_ac} 2302%We define that 2303\\ 2304A relation {\it R\/} 2305with 2306%is a {\it \quotient{} relation\/} with respect to 2307abstraction function {\it abs\/} 2308% and representation function {\it rep\/} 2309(between the representation type $\tau$ and the abstraction type $\xi$) 2310is a {\it quotient} 2311% (notated as $\langle R$,${\it abs}$,${\it rep} \rangle$) 2312(notated as $\langle R, {\it abs} \rangle$) 2313if and only if 2314%the following hold: 2315\end{definition} 2316 2317\begin{center} 2318\begin{tabular}[t]{l@{\hspace{0.5cm}}l} 2319%{\it existence of rep} 2320(1) 2321& $\forall a:\xi.\ \exists r:\tau.$ 2322{\it R\/} $r$ $r$ $\wedge$ ({\it abs\/} $r$ = $a$) \\ 2323%{\it partial equivalence} 2324(2) 2325& $\forall r\ s:\tau.$ 2326{\it R\/} $r$ $s$ $\Leftrightarrow$ 2327{\it R\/} $r$ $r$ $\wedge$ 2328{\it R\/} $s$ $s$ $\wedge$ 2329({\it abs} $r$ = {\it abs} $s$) \\ 2330\end{tabular} 2331\end{center} 2332 2333Property 1 states that for every abstract element $a$ of $\xi$ 2334there exists a representative in $\tau$ which respects {\it R\/} and whose abstraction is $a$. 2335%and lifts to $a$. 2336 2337Property 2 states that two elements of $\tau$ are related by {\it R\/} 2338if and only if 2339each element respects {\it R\/} and their abstractions are equal. 2340 2341The quotients for new quotient types 2342based on (partial) equivalence relations may now be 2343constructed by a modified version of \S \ref{quotienttypes}, 2344where the representation function {\it rep\/} is omitted 2345from Definition \ref{abs_rep_def}, so there is no 2346use of the Hilbert $\varepsilon$-operator. 2347Property 1 follows from Lemma \ref{ty_REP_REL}. 2348%and Property 2 2349%follows from Theorem 2350%\ref{equiv_ty_ABS}, as before. 2351% 2352The identity quotient is 2353$\langle \mbox{\tt \$=},\mbox{\tt I} \rangle$. 2354From Definition \ref{quotientdef_ac} 2355also follow analogs of the quotient extension theorems, e.g., 2356$$ 2357\forall R\ \mbox{\it abs}.\ \, 2358\langle R,\ \mbox{\it abs} \rangle \Rightarrow 2359\langle \mbox{\tt LIST\_REL}\ R,\ \mbox{\tt MAP}\ \mbox{\it abs} \rangle$$ 2360\noindent 2361for lists 2362and similarly for pairs, sums and option types. 2363Functions are lifted by 2364the abstraction operation for functions, which requires two new definitions: 2365\begin{eqnarray*} 2366(abs \repofabs R) \ a \ r \ & \defeq & \ 2367R\ r\ r\ \wedge \ {\it abs}\ r = a 2368\\ 2369(reps \ \mbox{\tt +->} \ abs) \ f \ x \ & \defeq & \ 2370\iota \ ({\tt IMAGE}\ {\it abs}\ ({\tt IMAGE}\ f\ ({\it reps}\ x))) 2371\end{eqnarray*} 2372% 2373\begin{comment} 2374\begin{eqnarray*} 2375abs \repofabs R \ & \defeq & \ 2376\lambda a{\mbox{\tt :}\xi}.\ 2377\lambda r{\mbox{\tt :}\tau}.\ 2378R\ r\ r\ \wedge \ {\it abs}\ r = a 2379\\ 2380rep \ \mbox{\tt +->} \ abs \ & \defeq & \ 2381\lambda f 2382%:\alpha \rightarrow \beta 2383.\ \lambda x.\ 2384\iota \ ({\tt IMAGE}\ {\it abs}\ ({\tt IMAGE}\ f\ ({\it rep}\ x))) 2385\end{eqnarray*} 2386\end{comment} 2387 2388\noindent 2389%Constants are lifted using this abstraction operator {\tt +->}. 2390Note that for the identity quotient, $(\mbox{\tt I $\repofabs$ \$=}) = \mbox{\tt \$=}$. 2391 2392The critical quotient extension 2393theorem for functions has also been proven: 2394\begin{theorem}[Function quotient extension] 2395\label{functionquotient} 2396$$ 2397%\forall R_1\ {\it abs}_1\ R_2\ {\it abs}_2.\ 2398 \langle R_1,\ {\it abs}_1 \rangle \Rightarrow 2399 \langle R_2,\ {\it abs}_2 \rangle \Rightarrow 2400\langle R_1 \ \mbox{\tt ===>} \ R_2,\ 2401 ({\it abs}_1 \repofabs R_1) \ \mbox{\tt +->} \ {\it abs}_2 \rangle$$ 2402\end{theorem} 2403\noindent 2404Unfortunately, the proof requires using the Axiom of Choice. 2405In fact, this theorem implies the Axiom of Choice, in that it implies 2406the existence of an operator which obeys the axiom of the 2407Hilbert $\varepsilon$-operator, as seen by the following development. 2408 2409\begin{theorem}[Partial abstraction quotients] 2410\label{partabsquotient} 2411%If $f{\tt :} \alpha \rightarrow \beta$ is any function, 2412If $f$ is any function from type $\alpha$ to $\beta$, 2413and 2414%$Q{\tt :} \alpha \rightarrow {\tt bool}$ is any predicate, 2415$Q$ is any predicate on $\alpha$, 2416such that $\forall y{\tt :}\beta.\ \exists x{\tt :}\alpha.\ Q\ x \wedge (f\;x = y)$, 2417then the partial equivalence relation $R = \lambda r\;s.\ Q\ r \wedge Q\ s \wedge (f\;r = f\;s)$ 2418with abstraction function $f$ is a quotient ($\langle R,f \rangle$). 2419\end{theorem} 2420{\bf Proof:} 2421%The two properties of Definition \ref{quotientdef_ac} 2422Follows easily from substituting $R$ 2423in Definition \ref{quotientdef_ac} 2424%as defined above 2425and simplifying. 2426$\Box$ 2427 2428\begin{theorem}[Partial inverses exist] 2429\label{partinverses} 2430If $f$ is any function from type $\alpha$ to $\beta$, and $Q$ is any 2431predicate on $\alpha$, 2432such that $\forall y{\tt :}\beta.\ \exists x{\tt :}\alpha.\ Q\ x \wedge (f\ x = y)$, 2433then there exists a function $g$ such that 2434%$(\mbox{\tt \$=}\ \mbox{\tt ===>}\ R)\ g\ g \wedge 2435$f \circ g = {\tt I}$ 2436% \wedge 2437and 2438%$(\forall x.\ Q\ (g\ x))$. 2439$\forall y.\ Q\ (g\ y)$. 2440{\rm 2441%Due in part to Dr. 2442[William Schneeburger]} 2443\end{theorem} 2444{\bf Proof:} 2445Assuming the function quotient extension theorem 2446%(Th. 2447\ref{functionquotient}, 2448we apply it to two quotient theorems; 2449first, the identity quotient 2450$\langle \mbox{\tt \$=}, \mbox{\tt I} \rangle$ 2451for type $\beta$, and second, 2452the partial abstraction quotient $\langle R,f \rangle$ 2453from Theorem \ref{partabsquotient}. 2454This yields the quotient 2455$\langle \mbox{\tt \$=}\ \mbox{\tt ===>}\ R,\ 2456% (\mbox{\tt I $\repofabs$ \$=}) 2457 \mbox{\tt \$=}\ \mbox{\tt +->}\ f \rangle$, 2458since $(\mbox{\tt I $\repofabs$ \$=}) = \mbox{\tt \$=}$. 2459By Property 1 of Definition \ref{quotientdef_ac}, 2460$\forall a.\ \exists r.\ (\mbox{\tt \$=}\ \mbox{\tt ===>}\ R)\ r\ r \wedge 2461(( 2462\mbox{\tt \$=} 2463\ \mbox{\tt +->}\ f) r = a)$. 2464Specializing $a = {\tt I}:\beta \rightarrow \beta$, 2465and renaming $r$ as $g$, we obtain 2466$\exists g.\ (\mbox{\tt \$=}\ \mbox{\tt ===>}\ R)\:g\ g \wedge 2467(\mbox{\tt \$=}\ \mbox{\tt +->}\ f) g = {\tt I})$. 2468By the definition of $\mbox{\tt ===>}$, 2469$(\mbox{\tt \$=}\ \mbox{\tt ===>}\ R)\:g\ g$ is 2470$\forall x\ y.\ x = y \Rightarrow R\ (g\ x)\ (g\ y)$, 2471which simplifies by the definition of {\it R\/} to $\forall y.\ Q\ (g\ y)$. 2472The right conjunct is 2473$ 2474%\exists g.\ 2475(\mbox{\tt \$=}\ \mbox{\tt +->}\ f) g = {\tt I}$, 2476which by the definition of {\tt +->} is 2477%which is 2478$ 2479%\exists g. 2480(\lambda x.\ 2481\iota \ ({\tt IMAGE}\ {\it f}\ ({\tt IMAGE}\ g\ (\mbox{\tt \$=}\ x)))) 2482 = {\tt I}$. 2483But $\mbox{\tt \$=}\ x$ is the singleton $\{x\}$, 2484so since ${\tt IMAGE}\ {\it h}\ \{z\} = \{h\ z\}$, 2485$\iota \{z\} = z$, 2486and $(\lambda x.\ f\ (g\ x)) = f \circ g$, 2487this 2488%is equivalent 2489simplifies 2490to $ 2491%\exists g. 2492%(\lambda x.\ f\ (g\ x)) = {\tt I}$, 2493f \circ g = {\tt I}$, 2494and 2495the conclusion follows. 2496$\Box$ 2497 2498\begin{theorem}[Existence of Hilbert choice] 2499\label{hilbertchoice} 2500There exists an operator $c:(\alpha \rightarrow {\tt bool}) \rightarrow \alpha$ 2501which obeys the Hilbert choice axiom, 2502$\forall P\ x.\ P\ x \Rightarrow P\ (c\ P)$. 2503\end{theorem} 2504 2505{\bf Proof:} 2506In Theorem \ref{partinverses}, 2507let $Q = (\lambda(P{\tt :}\alpha \rightarrow {\tt bool},\ a{\tt :}\alpha).\ 2508 (\exists x.\ P\ x) \Rightarrow P\ a)$ 2509and $f = {\tt FST}$. Then its antecedent is 2510$\forall P'.\, \exists (P,a).\, ((\exists x. P\, x) \Rightarrow P\, a) \wedge ({\tt FST} (P,a) = P')$. 2511For any $P'$, 2512take $P = P'$, and 2513if $\exists x.\ P\ x$, 2514then take $a$ to be such an $x$. 2515Otherwise take $a$ to be any value of $\alpha$. 2516In either case the antecedent is true. 2517%So 2518Therefore 2519by Theorem \ref{partinverses} 2520there exists a function $g$ such that 2521${\tt FST} \circ g = {\tt I}$ 2522and 2523$\forall P.\ Q\ (g\ P)$, 2524which is 2525%$\forall P.\ {\bf let}\ (P,a) = g\ P\ {\bf in}\ 2526$\forall P.\ 2527(\exists x.\ ({\tt FST}\ (g\ P))\ x) \Rightarrow ({\tt FST}\ (g\ P))\ ({\tt SND}\ (g\ P))$. 2528The operator $c$ is 2529taken as ${\tt SND} \circ g$, 2530and 2531since ${\tt FST}\ (g\ P) = P$, 2532the Hilbert choice axiom follows. 2533$\Box$ 2534 2535\begin{comment} 2536{\bf Proof:} 2537In Theorem \ref{partinverses}, 2538take $Q = (\lambda(P{\tt :}\alpha \rightarrow {\tt bool},\ a{\tt :}\alpha).\ 2539 (\exists x.\ P\ x) \Rightarrow P\ a)$ 2540and $f = {\tt FST}$. Then its antecedent is 2541$\forall P.\ \exists (P,a).\ ((\exists x.\ P\ x) \Rightarrow P\ a) \wedge ({\tt FST} (P,a) = P)$. 2542For any $P$, if $\exists x.\ P\ x$, 2543then take $a$ to be such an $x$. 2544Otherwise take $a$ to be any value of $\alpha$. 2545In either case the antecedent is true. 2546%So 2547Therefore there exists a function $g$ such that 2548${\tt FST} \circ g = {\tt I}$ 2549and 2550$\forall P.\ {\bf let}\ (P,a) = g\ P\ {\bf in}\ ((\exists x.\ P\ x) \Rightarrow P\ a)$. 2551The operator $c$ is then taken as ${\tt SND} \circ g$, 2552and the Hilbert choice axiom follows. 2553$\Box$ 2554\end{comment} 2555 2556\vspace{2.0mm} 2557The significance of Theorem \ref{hilbertchoice} 2558is that even if we are able to avoid all use of the Axiom of Choice up to 2559this point, it is not possible to prove the function quotient extension 2560theorem \ref{functionquotient} without it. 2561This section's design may be used 2562to build a theory of quotients which is constructive and which extends 2563naturally to quotients of lists, pairs, sums, and options. 2564However, it is not possible 2565to extend it to higher order quotients while remaining constructive. 2566Therefore 2567the designs presented in this paper cannot be used to create higher order 2568quotients in strictly constructive theorem provers. 2569Alternatively, in theorem 2570provers like HOL which admit the Hilbert choice operator, 2571%there is no point 2572%in avoiding its use if we wish to enjoy higher order quotients 2573%although an automatic system for lifting theorems could be constructed, 2574%analogous to that for the main design, 2575if higher order quotients are desired, 2576there is no advantage in avoiding using the Axiom of Choice 2577through using the design of this section. 2578%as long as 2579The main design presented earlier is much simpler to automate. 2580 2581 2582\vfill 2583\pagebreak[4] 2584% 2585\section{Lifting Types, Constants, and Theorems} 2586% 2587\label{liftingall} 2588 2589The definition of new types corresponding to the quotients of 2590existing types by equivalence relations is called ``lifting'' 2591the types from a lower, more representational level to a higher, 2592more abstract level. Both levels describe similar objects, but 2593some details which are apparent at the lower level are no longer 2594visible at the higher level. The logic is simplified. 2595 2596However, simply forming a new type does not complete the quotient operation. 2597Rather, one wishes to recreate the 2598%significant parts of the 2599pre-existing logical environment at the new, 2600higher, and more abstract level. This includes not only the new 2601types, but also new versions of the constants that form and 2602manipulate values of those types, and also new versions of the 2603theorems that describe properties of those constants. All of these 2604%must be recreated at the higher level, in order to 2605form a logical layer, above which all the lower representational details 2606may be safely and forever forgotten. 2607 2608%Essentially what we wish to do is to consider the entire environment 2609%of tools and capabilities to prove theorems that existed at the lower 2610%level, and recreate those capabilities at the higher level. This has 2611%three basic steps: 2612% 2613%\begin{enumerate} 2614%\item Lift the types, 2615%\item Lift the definitions of constants (including functions) on those types, 2616%\item Lift the theorems about the properties of those constants. 2617%\end{enumerate} 2618 2619This can be done in a single call of the 2620main tool of this package. 2621%This one call 2622%defines the new types, lifts the definitions of constants, 2623%and proves at the higher level the lifted versions of theorems. 2624 2625\begin{verbatim} 2626define_quotient_types : 2627 {types: {name: string, 2628 equiv: thm} list, 2629 defs: {def_name: string, 2630 fname: string, 2631 func: Term.term, 2632 fixity: Parse.fixity} list, 2633 tyop_equivs : thm list, 2634 tyop_quotients : thm list, 2635 tyop_simps : thm list, 2636 respects : thm list, 2637 poly_preserves : thm list, 2638 poly_respects : thm list, 2639 old_thms : thm list} -> 2640 thm list 2641\end{verbatim} 2642 2643{\tt define\_quotient\_types} takes a single argument which is a 2644record with the following fields. 2645 2646{\it types\/} is a list of records, each of which contains two fields: 2647{\it name}, which is the name of a new quotient type to be created, and 2648{\it equiv}, which is 2649either 1) 2650a theorem that a binary relation {\it R\/} 2651is an equivalence relation 2652(see section \ref{equivalence}), 2653or 2)\ a theorem that {\it R\/} is a nonempty partial equivalence relation, 2654of the form 2655$$ 2656\vdash\ 2657(\exists x.\ R\ x\ x) \ \wedge \ 2658(\forall x\ y.\ R\ x\ y \ \Leftrightarrow \ 2659 R\ x\ x \wedge R\ y\ y \wedge (R\ x = R\ y)) 2660$$ 2661%, 2662%of the form: 2663% 2664%\begin{center} 2665%{\tt $\vdash\ \forall$x y. {\it R} x y = ({\it R} x = {\it R} y)} 2666%\end{center} 2667\noindent 2668or using the abbreviated forms 2669$\vdash \mbox{\tt EQUIV}\ R$ 2670or 2671$\vdash \mbox{\tt PARTIAL\_EQUIV}\ R$, respectively. 2672 2673{\it defs\/} is a list of records specifying the constants to be lifted. 2674Each record contains the following four fields: 2675{\it func\/} is an HOL term, which must be a single constant, which is the 2676constant to be lifted. 2677{\it fname\/} is the name of the new constant being defined as the lifted version of {\it func}. 2678{\it fixity\/} is the HOL fixity of the new constant being created, 2679as specified in the HOL structure {\tt Parse}. 2680{\it def\_name} is the name under which the new constant definition is to 2681be stored in the current theory. 2682%These fields, and the 2683The 2684process of defining lifted constants 2685%This 2686is described in 2687\S\ref{liftingdefs}. 2688%section \ref{liftingdefs}. 2689 2690{\it tyop\_equivs\/} is a list of equivalence extension theorems 2691for type operators 2692(see 2693%section 2694\S\ref{condequivs}). These are used for 2695bringing into regular form 2696theorems on new type operators, so that they can be lifted 2697(see sections \ref{restrictions} and 2698\ref{nonstandard}). 2699 2700{\it tyop\_quotients\/} is a list of quotient extension theorems 2701for type operators 2702(see 2703%section 2704\S\ref{condquotients}). These are used for lifting both constants 2705and theorems. 2706 2707{\it tyop\_simps\/} is a list of theorems used to simplify type operator 2708relations and map functions for identity quotients, e.g., 2709for pairs, 2710$\vdash (\mbox{\tt \$= \#\#\# \$=}) = \mbox{\tt \$=}$ and 2711$\vdash (\mbox{\tt I \#\# I}) = \mbox{\tt I}$, 2712or for lists, 2713$\vdash \mbox{\tt LIST\_REL \$=} = \mbox{\tt \$=}$ and 2714$\vdash \mbox{\tt MAP I} = \mbox{\tt I}$. 2715 2716The rest of the arguments refer to the general process of lifting theorems 2717over the quotients being defined, 2718as described in section \ref{liftingtheorems}. 2719 2720{\it respects\/} is a list of theorems about the respectfulness of the 2721constants being lifted. 2722These theorems are described in section 2723\ref{respectfulness}. 2724 2725{\it poly\_preserves\/} is a list of theorems about the preservation of 2726polymorphic constants in the HOL logic 2727across a quotient operation. 2728%as if they were definitions across the quotient operation. 2729In other words, they state that any quotient operation preserves these 2730constants as a homomorphism. 2731These theorems are described in section 2732\ref{polypreserves}. 2733 2734{\it poly\_respects\/} is a list of theorems showing the respectfulness 2735of the polymorphic constants mentioned in {\it poly\_preserves}. 2736These are 2737described in 2738\S 2739%section 2740\ref{polyrespects}. 2741 2742{\it old\_thms\/} is a list of theorems concerning the lower, representative 2743types and contants, which are to be automatically lifted and proved at the 2744higher, more abstract quotient level. 2745These theorems are described in section \ref{oldtheorem}. 2746 2747{\tt define\_quotient\_types} returns a list of theorems, which are the 2748lifted versions of the {\it old\_thms}. 2749 2750A similar function, 2751{\tt define\_quotient\_types\_rule}, takes a single argument which is a 2752record with the same fields as above except for {\it old\_thms}, 2753and returns an SML function of type {\tt thm -> thm}. 2754This result, typically called {\tt LIFT\_RULE}, 2755is then used to lift the old theorems individually, one at a time. 2756 2757In addition to these, two related functions, 2758{\tt define\_quotient\_full\_types} and 2759{\tt define\_quotient\_full\_types\_rule}, 2760are provided 2761that automatically include the standard pre-proven quotient, 2762equivalence, and simplification theorems relating 2763to the list, pair, sum, option, and function type operators, along with 2764all the pre-proven polymorphic respectfulness and preservation theorems 2765for many standard polymorphic operators of those theories in HOL. 2766Other type operators and/or polymorphic operators may be supported 2767by including their theorems in the appropriate input fields, which 2768are named the same as before. 2769 2770%This function is limited to a single quotient type, but may be 2771%more convenient when the generality of {\tt define\_quotient\_types} 2772%is not needed. 2773The function {\tt define\_quotient\_types\_full\_rule} 2774can be defined in terms of {\tt define\_quotient\_types\_rule} as 2775 2776\begin{verbatim} 2777fun define_quotient_types_full_rule 2778 {types, defs, tyop_equivs, tyop_quotients, tyop_simps, 2779 respects, poly_preserves, poly_respects} = 2780 let 2781 val tyop_equivs = tyop_equivs @ 2782 [LIST_EQUIV, PAIR_EQUIV, SUM_EQUIV, OPTION_EQUIV] 2783 val tyop_quotients = tyop_quotients @ 2784 [LIST_QUOTIENT, PAIR_QUOTIENT, 2785 SUM_QUOTIENT, OPTION_QUOTIENT, FUN_QUOTIENT] 2786 val tyop_simps = tyop_simps @ 2787 [LIST_MAP_I, LIST_REL_EQ, PAIR_MAP_I, PAIR_REL_EQ, 2788 SUM_MAP_I, SUM_REL_EQ, OPTION_MAP_I, OPTION_REL_EQ, 2789 FUN_MAP_I, FUN_REL_EQ] 2790 val poly_preserves = poly_preserves @ 2791 [CONS_PRS, NIL_PRS, MAP_PRS, LENGTH_PRS, APPEND_PRS, 2792 FLAT_PRS, REVERSE_PRS, FILTER_PRS, NULL_PRS, 2793 SOME_EL_PRS, ALL_EL_PRS, FOLDL_PRS, FOLDR_PRS, 2794 FST_PRS, SND_PRS, COMMA_PRS, CURRY_PRS, 2795 UNCURRY_PRS, PAIR_MAP_PRS, 2796 INL_PRS, INR_PRS, ISL_PRS, ISR_PRS, SUM_MAP_PRS, 2797 NONE_PRS, SOME_PRS, IS_SOME_PRS, IS_NONE_PRS, 2798 OPTION_MAP_PRS, 2799 FORALL_PRS, EXISTS_PRS, 2800 EXISTS_UNIQUE_PRS, ABSTRACT_PRS, 2801 COND_PRS, LET_PRS, 2802 I_PRS, K_PRS, o_PRS, C_PRS, W_PRS] 2803 val poly_respects = poly_respects @ 2804 [CONS_RSP, NIL_RSP, MAP_RSP, LENGTH_RSP, APPEND_RSP, 2805 FLAT_RSP, REVERSE_RSP, FILTER_RSP, NULL_RSP, 2806 SOME_EL_RSP, ALL_EL_RSP, FOLDL_RSP, FOLDR_RSP, 2807 FST_RSP, SND_RSP, COMMA_RSP, CURRY_RSP, 2808 UNCURRY_RSP, PAIR_MAP_RSP, 2809 INL_RSP, INR_RSP, ISL_RSP, ISR_RSP, SUM_MAP_RSP, 2810 NONE_RSP, SOME_RSP, IS_SOME_RSP, IS_NONE_RSP, 2811 OPTION_MAP_RSP, 2812 RES_FORALL_RSP, RES_EXISTS_RSP, 2813 RES_EXISTS_EQUIV_RSP, RES_ABSTRACT_RSP, 2814 COND_RSP, LET_RSP, 2815 I_RSP, K_RSP, o_RSP, C_RSP, W_RSP] 2816 in 2817 define_quotient_types_rule 2818 {types=types, 2819 defs=defs, 2820 tyop_equivs=tyop_equivs, 2821 tyop_quotients=tyop_quotients, 2822 tyop_simps=tyop_simps, 2823 respects=respects, 2824 poly_preserves=poly_preserves, 2825 poly_respects=poly_respects} 2826 end; 2827\end{verbatim} 2828 2829Furthermore, two more related functions, 2830{\tt define\_quotient\_types\_std} and 2831{\tt define\_quotient\_types\_std\_rule}, 2832are provided. 2833These are the same as the ``{\tt full}'' functions above, but 2834%do not provide 2835without the input record fields for 2836{\tt tyop\_equivs}, 2837{\tt tyop\_quotients}, 2838{\tt tyop\_simps}, 2839{\tt poly\_preserves}, or 2840{\tt poly\_respects}. 2841The ``{\tt std}'' functions may be the easiest to use, providing much of the 2842power of higher order quotients without the need for the user 2843to worry about choosing theorems to include. 2844For many applications the ``{\tt std}'' functions will be all that is needed. 2845 2846Similar to the above, 2847the {\tt define\_quotient\_types\_std} function 2848is defined in terms of {\tt define\_quotient\_types\_full} as 2849 2850\begin{verbatim} 2851fun define_quotient_types_std {types, defs, respects, old_thms} = 2852 define_quotient_types_full 2853 {types=types, defs=defs, 2854 tyop_equivs=[], tyop_quotients=[], 2855 tyop_simps=[], 2856 respects=respects, 2857 poly_preserves=[], poly_respects=[], 2858 old_thms=old_thms}; 2859\end{verbatim} 2860 2861For backwards compatibility with John Harrison's excellent quotients package \cite{Har98} 2862%to whom much credit is due, and 2863(which provided much inspiration), 2864the following function is also provided: 2865 2866\begin{verbatim} 2867define_equivalence_type : 2868 {name: string, 2869 equiv: thm, 2870 defs: {def_name: string, 2871 fname: string, 2872 func: Term.term, 2873 fixity: Parse.fixity} list, 2874 welldefs : thm list, 2875 old_thms : thm list} -> 2876 thm list 2877\end{verbatim} 2878 2879\noindent 2880%This function is limited to a single quotient type, but may be 2881%more convenient when the generality of {\tt define\_quotient\_types} 2882%is not needed. 2883This function is defined in terms of {\tt define\_quotient\_types} as 2884 2885\begin{verbatim} 2886fun define_equivalence_type {name,equiv,defs,welldefs,old_thms} = 2887 define_quotient_types 2888 {types=[{name=name, equiv=equiv}], defs=defs, tyop_equivs=[], 2889 tyop_quotients=[FUN_QUOTIENT], 2890 tyop_simps=[FUN_REL_EQ,FUN_MAP_I], respects=welldefs, 2891 poly_preserves=[FORALL_PRS,EXISTS_PRS], 2892 poly_respects=[RES_FORALL_RSP,RES_EXISTS_RSP], 2893 old_thms=old_thms}; 2894\end{verbatim} 2895 2896%\begin{verbatim} 2897%fun define_equivalence_type {name,equiv,defs,respects,old_thms} = 2898% define_quotient_types {types=[{name=name, equiv=equiv}], 2899% defs=defs, tyop_equivs=[], 2900% tyop_quotients=[], tyop_simps=[], 2901% respects=respects, poly_preserves=[], 2902% poly_respects=[], old_thms=old_thms}; 2903%\end{verbatim} 2904 2905 2906% 2907\section{New Quotient Type Definitions} 2908% 2909\label{newquotienttype} 2910 2911In this section we describe how 2912the function {\tt define\_quotient\_types} creates new quotient types. 2913It automates the reasoning described 2914in section \ref{quotienttypes}, 2915creating the quotient type as a new type in 2916the HOL logic. It also defines the mapping functions between the 2917types, 2918forming 2919a quotient 2920%relationship 2921%with the equivalence relation 2922as described in theorem 2923\ref{quotientthm}. 2924\begin{comment} 2925\ref{ty_ABS_REP}, 2926\ref{rep_respects}, 2927and 2928\ref{equiv_ty_ABS}. 2929\end{comment} 2930 2931%The new type is created by the quotient type package by internally 2932%making use of the HOL primitive, {\tt new\_type\_definition}. 2933All definitions are accomplished as definitional extensions of HOL, 2934and thus 2935preserve HOL's consistency. 2936%cannot introduce inconsistency. 2937%are completely secure. 2938 2939Before invoking {\tt define\_quotient\_types}, the user should define 2940a relation on the original type $\tau$, and prove that it is 2941either 1) 2942an equivalence relation on the original type $\tau$, as described 2943in section \ref{equivalence}, 2944%The equivalence relation should be 2945%expressed as a constant {\it R}, 2946%of type 2947%{\tt ty -> ty -> bool}. 2948%$\tau_1 \rightarrow \tau_1 \rightarrow \mbox{\tt bool}$. 2949%If this constant is called 2950%In the following we will call this constant 2951%{\it R}, 2952%The user should prove that {\it R\/} is indeed an equivalence relation, 2953as a theorem 2954of the form: 2955 2956\begin{center} 2957\begin{tabular}[t]{l@{\hspace{0.3cm}}l} 2958{\tt R\_EQUIV} & 2959%{\tt |- $\forall$a b. {\it R\/} a b $\Leftrightarrow$ ({\it R\/} a = {\it R\/} b)} \\ 2960$\vdash 2961(\forall x\ y.\ R\ x\ y \ \Leftrightarrow \ (R\ x = R\ y))$ 2962\end{tabular} 2963\end{center} 2964 2965\noindent 2966or 2) 2967that the relation is a nonempty partial equivalence relation, 2968%as a theorem 2969of the form 2970\begin{center} 2971\begin{tabular}[t]{l@{\hspace{0.3cm}}l} 2972{\tt R\_EQUIV} & 2973$\vdash 2974(\exists x.\ R\ x\ x) \ \wedge \ 2975(\forall x\ y.\ R\ x\ y \ \Leftrightarrow \ 2976 R\ x\ x \wedge R\ y\ y \wedge (R\ x = R\ y))$. 2977\end{tabular} 2978\end{center} 2979 2980\noindent 2981Equivalently, 2982%the theorem 2983{\tt R\_EQUIV} 2984may be of the form 2985$\vdash \mbox{\tt EQUIV}\ R$ 2986or 2987$\vdash \mbox{\tt PARTIAL\_EQUIV}\ R$, respectively. 2988These abbreviations are defined in the theorems 2989{\tt EQUIV\_def} and {\tt PARTIAL\_EQUIV\_def}. 2990Evaluating 2991{\tt define\_quotient\_types} with the 2992argument 2993\linebreak[4] 2994%field 2995{\tt types} 2996containing the record 2997\texttt{\{name="{\it tyname}",} {\tt equiv=R\_EQUIV\}} 2998automatically declares a new type {\it tyname} 2999in the HOL logic as the quotient type $\tau / {\it R}$, 3000which we will refer to from here on as $\xi$, 3001%with the user-specified name ``{\it tyname}'', 3002and 3003declares two new constants {\it abs} {\tt :} $\tau \rightarrow \xi$ 3004with name ``{\it tyname}{\tt \_ABS}'' 3005and {\it rep} {\tt :} $\xi \rightarrow \tau$ 3006with name ``{\it tyname}{\tt \_REP}'', 3007such that the relation {\it R\/} 3008with 3009%respect to 3010{\it abs\/} and 3011{\it rep\/} 3012is a quotient, 3013as described in 3014Definition~\ref{quotientdef} of 3015section~\ref{quotientrelation}. 3016% 3017The {\tt define\_quotient\_types} tool proves 3018the quotient theorem 3019%for {\it R}, {\it abs}, and {\it rep}, 3020\begin{center} 3021\tt 3022$\vdash$ 3023QUOTIENT {\it R\/} {\it abs\/} {\it rep} 3024\end{center} 3025according to the development of 3026Section~\ref{quotienttypes}, 3027and stores it in the current theory under 3028the automatically-generated name \mbox{\it tyname}{\tt \_QUOTIENT}. 3029 3030 3031% 3032\section{Lifting Definitions of Constants} 3033% 3034\label{liftingdefs} 3035 3036The previous section 3037(\S\ref{newquotienttype}) 3038%We have previously 3039dealt with lifting types across a quotient operation. 3040This section deals with lifting constants, including functions, 3041whose 3042types 3043%arguments and/or results 3044involve the lifted types. 3045 3046Evaluating {\tt define\_quotient\_types} with the 3047argument 3048field {\tt defs} 3049containing the record 3050\begin{verse} \tt 3051\hspace{\parindent} 3052\hspace{2.0cm} 3053\{ 3054def\_name = "{\it defname}", \\ 3055\hspace{2.0cm} 3056fname \ \ \ = "{\it fname}", \\ 3057\hspace{2.0cm} 3058func \ \ \ \ = {\it function}, \\ 3059\hspace{2.0cm} 3060fixity \ \ = {\it fixity} \} \\ 3061\end{verse} 3062 3063\noindent 3064automatically declares a new constant {\it fname} 3065as a lifted version of the existing constant {\it function}. 3066Here {\it function} is an HOL term which is a single existing constant 3067of the HOL logic. 3068The new constant {\it fname} is given the fixity specified as {\it fixity}; 3069this is typically {\tt Prefix}, but might be, e.g., 3070{\tt Infix(NONASSOC,150)}, 3071or some other fixity 3072as supported by the structure {\tt Parse}. 3073The definition of the new constant is stored in the current theory 3074under the name {\it defname}. 3075 3076The theorem which is produced as the definition of the new constant 3077has the same form as the preservation theorems of section \ref{polypreserves}, 3078but without antecedents. 3079%It is used only internally as an input to the later step of lifting theorems 3080%concerning this constant. Afterwards, 3081After the quotient operation, 3082the definition theorem will not usually be of further value, as 3083the lifted theorems will be the basis for all further proof efforts. 3084 3085Here are the values related to fixity from the structure {\tt Parse}: 3086\begin{verbatim} 3087LEFT : associativity 3088RIGHT : associativity 3089NONASSOC : associativity 3090 3091Infixl : int -> fixity 3092Infixr : int -> fixity 3093Infix : associativity * int -> fixity 3094Prefix : int -> fixity 3095Closefix : fixity 3096Suffix : int -> fixity 3097fixity : string -> fixity 3098\end{verbatim} 3099 3100%Here is an example of a list of definitions of lifted constants, from 3101%the lambda calculus: 3102% 3103%\begin{verbatim} 3104% defs = [{def_name="Var_def", fname="Var", 3105% func= (--`Var1`--), fixity=Prefix}, 3106% {def_name="App_def", fname="App", 3107% func= (--`App1`--), fixity=Prefix}, 3108% {def_name="Lam_def", fname="Lam", 3109% func= (--`Lam1`--), fixity=Prefix}, 3110% {def_name="HEIGHT_def", fname="HEIGHT", 3111% func= (--`HEIGHT1`--), fixity=Prefix}, 3112% {def_name="FV_def", fname="FV", 3113% func= (--`FV1`--), fixity=Prefix}, 3114% {def_name="SUB_def", fname="SUB", 3115% func= (--`SUB1`--), fixity=Prefix}, 3116% {def_name="FV_subst_def", fname="FV_subst", 3117% func= (--`FV_subst1`--), fixity=Prefix}, 3118% {def_name="SUBt_def", fname="SUBt", 3119% func= (--`SUB1t`--), fixity=Prefix}, 3120% {def_name="vsubst_def", fname="/", 3121% func= (--`$//`--), fixity=Infix(NONASSOC,150)} 3122% ] 3123%\end{verbatim} 3124 3125 3126% 3127\section{Lifting Theorems of Properties} 3128% 3129\label{liftingtheorems} 3130 3131Previously we have seen how to lift types, and how to lift constants 3132on those types. This section describes how to lift 3133general theorems 3134%theorems of general properties 3135on those constants, 3136to restate them in terms of the lifted versions of 3137the constants and prove them correct, 3138given the existing theorems relating the lower versions of the constants. 3139 3140This turns out to be a substantially more complex process than 3141those previously described for lifting types and functions. 3142Because of its difficulty, the {\tt define\_quotient\_types} tool 3143automates the process completely, 3144and greatly eases the entire task of forming quotients. 3145In order for the tool to work effectively and 3146exert its full power, several ingredients need to be provided 3147by the user in the form of lists of theorems that describe 3148key properties of the type operators and constants used 3149in the theorem to be lifted. These kinds of theorems will be 3150described in detail in the subsections that follow. 3151First we 3152review the arguments of 3153{\tt define\_quotient\_types} 3154for lifting theorems. 3155 3156\begin{verbatim} 3157define_quotient_types : 3158 {types: {name: string, equiv: thm} list, 3159 defs: {def_name: string, fname: string, 3160 func: Term.term, fixity: Parse.fixity option} list, 3161 tyop_equivs : thm list, 3162 tyop_quotients : thm list, 3163 tyop_simps : thm list, 3164 respects : thm list, 3165 poly_preserves : thm list, 3166 poly_respects : thm list, 3167 old_thms : thm list} -> 3168 thm list 3169\end{verbatim} 3170 3171\noindent 3172The last four fields of the argument to {\tt define\_quotient\_types} 3173are lists of theorems. The last field ({\tt old\_thms}) 3174is the list of theorems to be lifted, and the 3175result produced by the tool is 3176the list of the lifted versions of those theorems. 3177The meanings of the other three fields 3178({\tt respects}, {\tt poly\_preserves}, {\tt poly\_respects}) 3179are described in the following subsections. 3180 3181%The theory {\tt quotientTheory} provides a number 3182%of theorems about the well-definedness and respectfulness of 3183%many common operators for lists, products, sums, options, and function types. 3184%These theorems ease the automation of the process of lifting theorems 3185%that use these common operators and 3186%involve the original types to their corresponding versions involving the 3187%quotient types. For other operators not included, the script that 3188%creates the theory provides examples of how to prove such theorems, 3189%which is usually not difficult. 3190 3191 3192%\begin{enumerate} 3193 3194% 3195\subsection{Respectfulness theorems: {\tt respects}} 3196% 3197\label{respectfulness} 3198 3199%\item 3200{\tt respects} is a list of theorems demonstrating the 3201respectfulness of all constants used in {\tt old\_thms} 3202(except polymorphic operators). 3203These state that for each such constant, 3204considered as a function, 3205the equivalence class of the result yielded 3206depends only on the equivalence classes of the inputs, 3207not on any input's particular 3208value 3209%choice of representative 3210within the class. 3211 3212Not all functions defined at the lower level 3213respect the equivalence relations involved in the 3214lifting process. Theorems that mention such disrespectful functions 3215cannot in general be lifted. 3216The respectfulness of each function involved must be 3217demonstrated through a theorem of the general form 3218 3219\begin{center} 3220\begin{tabular}{rl} 3221$\vdash$& 3222{\tt $\forall$(x1:$\gamma_1$) (y1:$\gamma_1$) ... (xn:$\gamma_n$) (yn:$\gamma_n$).} 3223\\ 3224& \hspace{12mm} 3225{\tt $R_1$ x1 y1 \ 3226$\wedge$ \ 3227... \ 3228$\wedge$ \ 3229$R_n$ xn yn \;$\Rightarrow$ 3230} \\ 3231& \hspace{12mm} 3232{\tt $R_c$ (C x1 ... xn) (C y1 ... yn)} \\ 3233\end{tabular} 3234\end{center} 3235where the constant {\tt C} has type 3236{\tt $\gamma_1$ -> ... -> $\gamma_n$ -> $\gamma_c$} ($n \ge 0$), 3237and each relation {\tt $R_i$} has type {\tt $\gamma_i$ -> $\gamma_i$ -> bool} 3238for all $i$. 3239Depending on the types involved, 3240the \quotient{} relations $R_1$, ..., $R_n$, $R_c$ 3241may be simple equality, equivalence relations, 3242aggregate \quotient{} relations, 3243or higher-order \quotient{} relations (see section \ref{aggregates}), 3244as illustrated in examples below. 3245 3246In fact, in the special case where one of the relations $R_i$ is simple 3247equality (which happens when the type 3248%involved 3249$\gamma_i$ is not a type being lifted), 3250the above general form may be simplified, in the following ways. 3251The two variables {\tt xi} and {\tt yi} may be combined into one, 3252say {\tt (zi:$\gamma_i$)}, e.g. in the list of universally quantified variables. 3253The antecedent conjunct {\tt $R_i$ xi yi}, which here is {\tt xi = yi}, 3254may be omitted. In the conclusion {\tt $R_c$ (C x1 ... xn) (C y1 ... yn)}, 3255the same variable {\tt zi} may be used in place of both {\tt xi} in the first 3256operand of {\tt $R_c$} and {\tt yi} in the second operand. This simpler 3257version is not completely standard, but may be more convenient for 3258the user to provide. The package will compensate by automatically 3259creating the standard version from this simplified one. 3260Also, if all the antecedents thus simplify, 3261or if $n = 0$ with no antecedents, 3262then the implication 3263simplifies 3264%collapses 3265to just the consequent, {\tt $R_c$ (C z1 ... zn) (C z1 ... zn)}. 3266 3267To illustrate this, the following functions are taken from an example 3268of syntactic terms of the untyped lambda calculus, 3269where the term type {\tt term1} 3270is being lifted to a new type {\tt term} 3271by identifying terms that are equivalent 3272according to the equivalence relation {\tt ALPHA: term1 -> term1 -> bool}. 3273 3274The function {\tt Var1 : var -> term1} is used to construct 3275lambda calculus terms which are single variables. 3276The respectfulness theorem for {\tt Var1} is 3277{\tt \begin{tabbing} 3278\hspace{5.5mm} 3279 $\vdash \forall$x1 x2. (x1 = x2) $\Rightarrow$ ALPHA (Var1 x1) (Var1 x2) 3280\end{tabbing}} 3281\pagebreak[2] 3282\noindent 3283or possibly the simplified (but nonstandard) form 3284{\tt \begin{tabbing} 3285\hspace{5.5mm} 3286 $\vdash \forall$x. ALPHA (Var1 x) (Var1 x) 3287\end{tabbing}} 3288{\tt Var1} has one argument of type {\tt var}, which type is not lifted, 3289so the \quotient{} relation of this argument is simple equality. 3290The result type is {\tt term1}, so the \quotient{} relation for the 3291result is {\tt ALPHA}. 3292 3293The function {\tt App1 : term1 -> term1 -> term1} 3294is used to construct terms which are applications of a function to an argument. 3295The respectfulness theorem for {\tt App1} is 3296{\tt \begin{tabbing} 3297\hspace{5.5mm} 3298 $\vdash \forall$t\=1 t2 u1 u2. \\ 3299\> ALPHA t1 t2 $\wedge$ ALPHA u1 u2 $\Rightarrow$\\ 3300\> ALPHA (App1 t1 u1) (App1 t2 u2) 3301\end{tabbing}} 3302{\tt App1} has two arguments. 3303The first argument has type {\tt term1}, 3304so the \quotient{} relation of this argument is {\tt ALPHA}. 3305The second argument also has type {\tt term1}, 3306so the \quotient{} relation of this argument is also {\tt ALPHA}. 3307The result type is {\tt term1}, so the \quotient{} relation for the 3308result is {\tt ALPHA}. 3309 3310The function {\tt HEIGHT1 : term1 -> num} 3311is used to calculate the height of a term as a tree. 3312The respectfulness theorem for {\tt HEIGHT1} is 3313{\tt \begin{tabbing} 3314\hspace{5.5mm} 3315 $\vdash \forall$t1 t2. ALPHA t1 t2 $\Rightarrow$ (HEIGHT1 t1 = HEIGHT1 t2) 3316\end{tabbing}} 3317{\tt HEIGHT1} has one argument, which 3318has type {\tt term1}, 3319so the \quotient{} relation of the argument is {\tt ALPHA}. 3320The result type is {\tt num}, which is not being lifted, 3321so the \quotient{} relation for the result is simple equality. 3322 3323The function {\tt FV1 : term1 -> (var -> bool)} 3324is used to calculate the set of free variables of a term. 3325The respectfulness theorem for {\tt FV1} is 3326{\tt \begin{tabbing} 3327\hspace{5.5mm} 3328 $\vdash \forall$t1 t2. ALPHA t1 t2 $\Rightarrow$ (FV1 t1 = FV1 t2) 3329\end{tabbing}} 3330{\tt FV1} has one argument, which 3331has type {\tt term1}, 3332so the \quotient{} relation of the argument is {\tt ALPHA}. 3333The result type is {\tt var -> bool}. 3334Even though this is a functional type, 3335it is not affected by lifting, 3336so the \quotient{} relation for the result is simple equality. 3337 3338The function {\tt <[ : term1 -> (var \# term1) list -> term1} 3339is used to simultaneously substitute a list of terms 3340for a corresponding list of variables 3341where they occur free across a target term. 3342The respectfulness theorem for {\tt <[} is 3343{\tt \begin{tabbing} 3344\hspace{5.5mm} 3345 $\vdash \forall$t\=1 t2 s1 s2. \\ 3346\> ALPHA t1 t2 $\wedge$ LIST\_REL (\$= \#\#\# ALPHA) s1 s2 $\Rightarrow$ \\ 3347\> ALPHA (t1 <[ s1) (t2 <[ s2) 3348\end{tabbing}} 3349{\tt <[} has two arguments. 3350The first argument has type {\tt term1}, 3351so the \quotient{} relation of this argument is {\tt ALPHA}. 3352The second argument is a substitution, which has type {\tt (var \# term1) list}, 3353so the \quotient{} relation of this argument is {\tt LIST\_REL (\$= \#\#\# ALPHA)}. 3354The result type is {\tt term1}, so the \quotient{} relation for the 3355result is {\tt ALPHA}. 3356 3357%Consider the following nine functions, taken from an example of terms of the 3358%lambda calculus, where the term type {\tt term1} is being lifted to a new 3359%type {\tt term} according to the equivalence relation 3360%{\tt ALPHA: term1 -> term1 -> bool}. 3361%\begin{center} 3362%{\tt 3363%\begin{tabular}{lcl} 3364%Var1 & : & var -> term1 \\ 3365%App1 & : & term1 -> term1 -> term1 \\ 3366%Lam1 & : & var -> term1 -> term1 \\ 3367%HEIGHT1 & : & term1 -> num \\ 3368%FV1 & : & term1 -> (var -> bool) \\ 3369%SUB1 & : & (var \# term1) list -> var -> term1 \\ 3370%FV\_subst1 & : & (var \# term1) list -> (var -> bool) -> (var -> bool) \\ 3371%\$// & : & var list -> var list -> (var \# term1) list \\ 3372%\$<[ & : & term1 -> (var \# term1) list -> term1 \\ 3373%\end{tabular} 3374%} 3375%\end{center} 3376% 3377%\noindent 3378%Then the following nine theorems show the respectfulness of these functions: 3379%\begin{verbatim} 3380% |- !x1 x2. (x1 = x2) ==> ALPHA (Var1 x1) (Var1 x2) 3381% |- !t1 t2 u1 u2. 3382% ALPHA t1 t2 /\ ALPHA u1 u2 3383% ==> ALPHA (App1 t1 u1) (App1 t2 u2) 3384% |- !x1 x2 t1 t2. 3385% (x1 = x2) /\ ALPHA t1 t2 3386% ==> ALPHA (Lam1 x1 t1) (Lam1 x2 t2) 3387% |- !t1 t2. ALPHA t1 t2 ==> (HEIGHT1 t1 = HEIGHT1 t2) 3388% |- !t1 t2. ALPHA t1 t2 ==> (FV1 t1 = FV1 t2) 3389% |- !s1 s2 x1 x2. 3390% LIST_REL ($= ### ALPHA) s1 s2 /\ (x1 = x2) ==> 3391% ALPHA (SUB1 s1 x1) (SUB1 s2 x2) 3392% |- !s1 s2 xs ys. 3393% LIST_REL ($= ### ALPHA) s1 s2 /\ (xs = ys) ==> 3394% (FV_subst1 s1 xs = FV_subst1 s2 ys) 3395% |- !xs1 xs2 ys1 ys2. 3396% (xs1 = xs2) /\ (ys1 = ys2) ==> 3397% LIST_REL ($= ### ALPHA) (xs1 // ys1) (xs2 // ys2) 3398% |- !t1 t2 s1 s2. 3399% ALPHA t1 t2 /\ LIST_REL ($= ### ALPHA) s1 s2 ==> 3400% ALPHA (t1 <[ s1) (t2 <[ s2) 3401%\end{verbatim} 3402 3403%val respects = [Var1_ALPHA, App1_ALPHA, Lam1_ALPHA, ALPHA_HEIGHT, 3404% ALPHA_FV, SUB1_RSP, FV_subst_RSP, vsubst1_RSP, SUBt_RSP] 3405% 3406% \begin{verbatim} 3407% > val respects = 3408% [|- !x1 x2. (x1 = x2) ==> ALPHA (Var1 x1) (Var1 x2), 3409% |- !t1 t2 u1 u2. 3410% ALPHA t1 t2 /\ ALPHA u1 u2 ==> 3411% ALPHA (App1 t1 u1) (App1 t2 u2), 3412% |- !x1 x2 t1 t2. 3413% (x1 = x2) /\ ALPHA t1 t2 ==> 3414% ALPHA (Lam1 x1 t1) (Lam1 x2 t2), 3415% |- !t1 t2. ALPHA t1 t2 ==> (HEIGHT1 t1 = HEIGHT1 t2), 3416% 3417% |- !t1 t2. ALPHA t1 t2 ==> (FV1 t1 = FV1 t2), 3418% |- !s1 s2 x1 x2. 3419% LIST_REL ($= ### ALPHA) s1 s2 /\ (x1 = x2) ==> 3420% ALPHA (SUB1 s1 x1) (SUB1 s2 x2), 3421% |- !s1 s2 xs ys. 3422% LIST_REL ($= ### ALPHA) s1 s2 /\ (xs = ys) ==> 3423% (FV_subst1 s1 xs = FV_subst1 s2 ys), 3424% |- !xs1 xs2 ys1 ys2. 3425% (xs1 = xs2) /\ (ys1 = ys2) ==> 3426% LIST_REL ($= ### ALPHA) (xs1 // ys1) (xs2 // ys2), 3427% |- !t1 t2 s1 s2. 3428% ALPHA t1 t2 /\ LIST_REL ($= ### ALPHA) s1 s2 ==> 3429% ALPHA (t1 <[ s1) (t2 <[ s2)] : thm list 3430% \end{verbatim} 3431 3432% These nine theorems show the respectfulness of the functions 3433% {\tt Var1}, {\tt App1}, 3434% {\tt Lam1}, {\tt HEIGHT1}, 3435% {\tt FV1}, {\tt SUB1}, 3436% {\tt FV\_subst1}, 3437% {\tt //}, and {\tt <[}. 3438 3439Please note how the antecedents of each theorem relate to the arguments 3440of the function. The arguments which have types not being lifted 3441are compared by equality, while the arguments which have types being lifted 3442are compared by the corresponding \quotient{} relation. Similarly, the 3443consequent of each of the theorems above is either a \quotient{} or an 3444equality, depending on whether the type of the value returned by the 3445function is of a type being lifted or not. There is a direct one-to-one 3446relationship between the type of the argument/result and the 3447\quotient{} relation used to compare its values. 3448 3449Therefore the antecedent of the theorem on the respectfulness of {\tt Var1} 3450is an equality, since the type of the argument is {\tt var} which is not 3451being lifted, while the antecedents of the theorem on the respectfulness 3452of {\tt App1} are both \quotient{}s, since the type of those arguments is 3453{\tt term1}, which is being lifted according to the equivalence relation 3454{\tt ALPHA}. Also, the consequent of the theorem on the respectfulness 3455of {\tt HEIGHT1} is an equality, since the type of the value returned 3456by {\tt HEIGHT1} is {\tt num}, which is not being lifted. If the 3457arguments and the value returned by a function are all of types 3458not being lifted, then there is no need for a respectfulness theorem 3459for that function. 3460 3461Also, where a function has an argument of an aggregate type, 3462the corresponding \quotient{} relation is created by an aggregate operator. 3463For example, in the theorem on the respectfulness of 3464{\tt <[}, the 3465%second argument has type 3466type of the second argument is 3467{\tt (var \# term1) list}. 3468The 3469\quotient{} 3470relation that corresponds to this type is 3471{\tt LIST\_REL (\$= \#\#\# ALPHA)}, 3472constructed by first 3473using the {\tt \#\#\#} operator to create the 3474%\quotient{} 3475relation for 3476{\tt var \# term1}, 3477and then using the {\tt LIST\_REL} 3478operator to create the 3479%\quotient{} 3480relation for 3481{\tt (var \# term1) list}. 3482These \quotient{} relation operators 3483are described in section \ref{aggregates}. 3484 3485Whenever there are arguments to the constant, there are 3486multiple equivalent ways to state the respectfulness theorem. 3487For example, the respectfulness theorem for {\tt FV1:term1 -> var -> bool} may be given 3488equally well as any of the following completely equivalent versions: 3489{\tt \begin{tabbing} 3490\hspace{5.5mm} 3491 \=$\vdash \forall$t\=1 t2 x1 x2. \\ 3492\>\> ALPHA t1 t2 $\wedge$ (x1 = x2) $\Rightarrow$ (FV1 t1 x1 = FV1 t2 x2) \\ 3493\> $\vdash \forall$t1 t2. ALPHA t1 t2 $\Rightarrow$ (FV1 t1 = FV1 t2) \\ 3494\> $\vdash$ (ALPHA ===> \$=) FV1 FV1 3495\end{tabbing}} 3496The last version has higher order and lesser arity than the 3497earlier versions. In fact, the three theorems above have arities 34982, 1, and 0, respectively, 3499while the last theorem is the only one with a 3500higher order \quotient{} relation. 3501The earlier versions may be easier to understand and prove than the 3502last version. For the quotient package's internal use, all respectfulness 3503theorems are automatically converted to the highest order and lowest 3504arity possible, usually with arity zero. 3505 3506 3507% 3508\subsection{ 3509Preservation 3510%``Definitions'' 3511of polymorphic functions: {\tt poly\_preserves}} 3512% 3513\label{polypreserves} 3514 3515%\item 3516{\tt poly\_preserves} is a list of theorems expressing the preservation 3517of generic, polymorphic functions across quotient operations. 3518%such as {\tt NIL}, {\tt LENGTH}, {\tt CONS}, {\tt FST}, and {\tt o}. 3519This is expressed as an 3520equality between the value of the function applied to arguments of 3521lifted types, and the lifted version of the value of the same function 3522applied to arguments of the lower types. 3523The equalities are conditioned on the component types being quotients. 3524 3525These preservation theorems have the following general form. 3526\begin{center} 3527\begin{tabular}{rl} 3528$\vdash$ 3529& {\tt $\forall$R1 (abs1:$\alpha_1$->$\beta_1$) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$} \\ 3530& {\tt ...} \\ 3531& {\tt $\forall$Rn (absn:$\alpha_n$->$\beta_n$) repn. QUOTIENT Rn absn repn $\Rightarrow$} \\ 3532& {\tt $\forall$(x1:$\delta_1$) ... (xk:$\delta_k$).} \\ 3533& \hspace{17mm} 3534{\tt C' x1 ... xk = $abs_c$ (C ($rep_1$ x1) ... ($rep_k$ xk)) } \\ 3535\end{tabular} 3536\end{center} 3537where 3538\begin{enumerate} 3539\item 3540the constant {\tt C} has a polymorphic type with $n>0$ type variables, 3541$\alpha_1, ..., \alpha_n$, 3542%where $n > 0$, 3543% and where 3544\item 3545{\tt C'} is usually {\tt C}, but may be a different constant 3546in case {\tt C} is not preserved, 3547% and where 3548\item 3549the type of {\tt C} is of the form 3550{\tt $\gamma_1$ -> ... -> $\gamma_k$ -> $\gamma_c$} ($k \ge 0$) \\ 3551({\tt C} is a curried function of $k$ arguments, with a return value of 3552type $\gamma_c$), \\ 3553with 3554all type variables in the $\gamma_1$, ..., $\gamma_k$, $\gamma_c$ types 3555contained within $\alpha_1$,~...,~$\alpha_n$, 3556% and where 3557\item 3558the type of {\tt C'} is of the form 3559{\tt $\delta_1$ -> ... -> $\delta_k$ -> $\delta_c$} ($k \ge 0$) \\ 3560({\tt C'} is a curried function of $k$ arguments, with a return value of 3561type $\delta_c$), 3562% and where 3563\item 3564$\delta_i$ is the lifted version of $\gamma_i$ for all $i=1,...,k,c$ \\ 3565($\delta_i = \gamma_i[\alpha_j \mapsto \beta_j \mbox{\ for all\ } j=1,...,n]$), 3566%($\delta_i = \gamma_i[\alpha_i \mapsto \beta_i \forall i=1,...,n]$), 3567\\ 3568with 3569all type variables in the $\delta_1$, ..., $\delta_k$, $\delta_c$ types 3570contained within $\beta_1$,~...,~$\beta_n$, 3571and 3572\item 3573{\tt $abs_i$:$\gamma_i$ -> $\delta_i$} and 3574{\tt $rep_i$:$\delta_i$ -> $\gamma_i$} 3575are the (possibly identity, aggregate, or higher-order) 3576abstraction and representation functions 3577for the type $\gamma_i$, for all $i=1,...,k,c$. 3578These are expressions, not simply an 3579{\tt absi} or {\tt repi} variable. 3580\end{enumerate} 3581 3582Depending on the types involved, some 3583of the abstraction or representation functions 3584%{\tt absj}, {\tt repj}, ..., {\tt Rk}, {\tt Rt} 3585may be the identity function {\tt I}, in which case they disappear, 3586as illustrated in some of the examples below. 3587 3588For clarity, we will discuss examples for particular polymorphic operators, 3589beginning with simpler ones. 3590In each case, the main driver of the form of the resulting theorem is the 3591the operator's type, in particular the number of arguments, the type of 3592each argument, and the type returned by the operator. 3593 3594The preservation theorem for {\tt NIL} is 3595{\tt \begin{tabbing} 3596\hspace{5.5mm} 3597 $\vdash \forall$R (a\=bs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\ 3598\> ([] = MAP abs []) 3599\end{tabbing}} 3600The operator {\tt NIL} has polymorphic type {\tt ('a)list}. 3601It has one type variable, {\tt 'a}, so $n = 1$. 3602It has no arguments, so $k = 0$. 3603The result type is 3604%$\gamma_c$ = 3605{\tt ('a)list}, 3606%The lifted version of this type is 3607%$\delta_c$ = {\tt ('b)list}. 3608for which 3609the abstraction function 3610%for $\gamma_c$ 3611is {\tt MAP abs}. 3612 3613\pagebreak[2] 3614The preservation theorem for {\tt LENGTH} is 3615{\tt \begin{tabbing} 3616\hspace{5.5mm} 3617 $\vdash \forall$R\=\ (abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\ 3618\> $\forall$l. LENGTH l = LENGTH (MAP rep l) 3619\end{tabbing}} 3620The operator {\tt LENGTH} has polymorphic type {\tt ('a)list -> num}. 3621It has one type variable, {\tt 'a}, so $n = 1$. 3622It has one argument, so $k = 1$. 3623The argument type is 3624%$\gamma_1$ = 3625{\tt ('a)list}, 3626for which 3627the representation function 3628%for $\gamma_1$ 3629is {\tt MAP rep}. 3630The result type is 3631%$\gamma_c$ = 3632{\tt num}, 3633for which 3634%The lifted versions of these types are 3635%$\delta_1$ = {\tt ('b)list}, 3636%$\delta_c$ = {\tt num}. 3637the abstraction function 3638%for $\gamma_c$ 3639is {\tt I}, which disappears. 3640 3641\pagebreak[2] 3642The preservation theorem for {\tt CONS} is 3643{\tt \begin{tabbing} 3644\hspace{5.5mm} 3645 $\vdash \forall$R\=\ (abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\ 3646\> $\forall$t h. h::t = MAP abs (rep h::MAP rep t) 3647\end{tabbing}} 3648The operator {\tt CONS} has polymorphic type {\tt 'a -> ('a)list -> ('a)list}. 3649It has one type variable, {\tt 'a}, so $n = 1$. 3650It has two arguments, so $k = 2$. 3651The first argument type is 3652%$\gamma_1$ = 3653{\tt 'a}, 3654for which 3655the representation function 3656%for $\gamma_1$ 3657is {\tt rep}. 3658The second argument type is 3659%$\gamma_2$ = 3660{\tt ('a)list}, 3661for which 3662the representation function 3663%for $\gamma_2$ 3664is {\tt MAP rep}. 3665The result type is 3666%$\gamma_c$ = 3667{\tt ('a)list}, 3668for which 3669the abstraction function 3670%for $\gamma_c$ 3671is {\tt MAP abs}. 3672%The lifted versions of these types are 3673%$\delta_1$ = {\tt 'b}, 3674%$\delta_2$ = {\tt ('b)list}, 3675%$\delta_c$ = {\tt ('b)list}. 3676 3677The preservation theorem for {\tt FST} is 3678{\tt \begin{tabbing} 3679\hspace{5.5mm} 3680 $\vdash$ \=$\forall$R\=1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\ 3681\> $\forall$R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\ 3682\>\> $\forall$p:'c \# 'd. FST p = abs1 (FST ((rep1 \#\# rep2) p)) 3683\end{tabbing}} 3684The operator {\tt FST} has polymorphic type {\tt ('a \# 'b) -> 'a}. 3685It has two type variables, {\tt 'a} and {\tt 'b}, so $n = 2$. 3686It has one argument, so $k = 1$. 3687The argument type is 3688%$\gamma_1$ = 3689{\tt ('a \# 'b)}, 3690for which 3691the representation function 3692%for $\gamma_1$ 3693is {\tt rep1 \#\# rep2}. 3694The result type is 3695%$\gamma_c$ = 3696{\tt 'a}, 3697for which 3698the abstraction function 3699%for $\gamma_c$ 3700is {\tt abs1}. 3701%The lifted versions of these types are 3702%$\delta_1$ = {\tt ('c \# 'd)}, 3703%$\delta_c$ = {\tt 'c}. 3704 3705\pagebreak[3] 3706The preservation theorem for the composition operator {\tt o} is 3707{\tt \begin{tabbing} 3708\hspace{5.5mm} 3709 $\vdash$ \=$\forall$R\=1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\ 3710\> $\forall$R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\ 3711\> $\forall$R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 $\Rightarrow$ \\ 3712\>\> $\forall$f\=\ g. f o g = \\ 3713\>\>\> (rep1 --> abs3) ((abs2 --> rep3) f o (abs1 --> rep2) g) 3714\end{tabbing}} 3715The operator {\tt o} has type 3716{\tt ('b ->\;'c) -> ('a ->\;'b) -> ('a ->\;'c)}, 3717which is polymorphic and also higher order. 3718It has three type variables, {\tt 'a}, {\tt 'b}, and {\tt 'c}, so $n = 3$. 3719It has two arguments, so $k = 2$. 3720The first argument type is 3721%$\gamma_1$ = 3722{\tt 'b -> 'c}, 3723for which 3724the representation function 3725%for $\gamma_1$ 3726is {\tt abs2 --> rep3}. 3727The second argument type is 3728%$\gamma_2$ = 3729{\tt 'a -> 'b}, 3730for which 3731the representation function 3732%for $\gamma_2$ 3733is {\tt abs1 --> rep2}. 3734The result type is 3735%$\gamma_c$ = 3736{\tt 'a -> 'c}, 3737for which 3738the abstraction function 3739%for $\gamma_c$ 3740is {\tt rep1 --> abs3}. 3741%The lifted versions of these types are 3742%$\delta_1$ = {\tt 'e -> 'f}, 3743%$\delta_1$ = {\tt 'd -> 'e}, 3744%$\delta_c$ = {\tt 'd -> 'f}. 3745 3746%Because the operator {\tt o} returns a higher-order result, the operator 3747%could be considered to have three arguments, not two, where the type of 3748%the third argument is {\tt 'a}, for which the representation function 3749%is {\tt rep1}, and where the result type is {\tt 'c}, for which the 3750%abstraction function is {\tt abs3}. This choice would give rise to 3751%the following variant definition theorem. Either choice is fine. 3752%\begin{verbatim} 3753% |- !R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==> 3754% !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==> 3755% !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==> 3756% !f g x. (f o g) x = 3757% abs3 (((abs2 --> rep3) f o (abs1 --> rep2) g) (rep1 x)) 3758%\end{verbatim} 3759 3760 3761Since the types of 3762these functions are polymorphic, instances of the functions may be applied 3763on arguments of either the types being lifted or the higher, lifted types. 3764In a style very similar to the definition theorems constructed 3765by {\tt define\_quotient\_types} for the new versions of the 3766constants being lifted, 3767each theorem expresses that the value of 3768the operator applied to arguments of the lifted types 3769is equal to the lifted version of the value of the same operator 3770applied to arguments of the lower types, 3771computed by lowering the original arguments. 3772 3773So for example, in the {\tt CONS} example above, 3774the {\tt CONS} operator is equal to taking its arguments 3775{\tt h} and {\tt t}, lowering each argument as {\tt rep h} and {\tt MAP rep t}, 3776then applying {\tt CONS} to these two lowered arguments to compute the 3777result at the lower level, and then raising the result to the lifted level 3778by {\tt MAP abs}. 3779 3780These 3781express the use of each polymorphic function at the 3782lifted level in terms of its use at the lower level. 3783 3784These theorems differ from 3785the definition theorems for new constants 3786is that each theorem conditions the preservation statement 3787upon the polymorphic types being 3788proper quotients. The conditions follow the form 3789of a quotient theorem as given in section \ref{newquotienttype}, 3790but each describes a quotient for a polymorphic type variable 3791instead of for a specific type. If the function is polymorphic in more 3792than one type, then the theorem will be conditioned on all of the 3793type variables being quotient types. 3794 3795Thus in the {\tt o} example above, the preservation 3796of the composition operator {\tt o} 3797is conditioned on three types being lifted, 3798where {\tt 'a} is being lifted to {\tt 'd}, 3799{\tt 'b} is being lifted to {\tt 'e}, and 3800{\tt 'c} is being lifted to {\tt 'f}. 3801This calls for three antecedents which are quotient theorems of {\tt 'a}, 3802{\tt 'b}, and {\tt 'c}. 3803In a theorem to be lifted, when 3804the composition operator is actually applied 3805to arguments which are functions from specific domains 3806to specific ranges, the {\tt o} preservation theorem will be 3807instantiated with those types, 3808to be resolved against actual quotient theorems for those types. 3809 3810A substantial collection of these 3811preservation 3812%``definition'' 3813theorems for various 3814standard polymorphic functions of the HOL logic have been proven already and 3815is available in the theories of the quotient library (see Table 1). 3816If there is a need to use a 3817polymorphic function not covered by these, the corresponding 3818preservation 3819%``definition'' 3820theorem can be proven by the user, using the same approach as for the example 3821theorems above, as shown in the theory scripts of the quotient library. 3822 3823Whenever there are arguments to the constant, there are 3824multiple equivalent ways to state the 3825preservation 3826%``definition'' 3827theorem. 3828For example, the consequent of the 3829preservation 3830%``definition'' 3831theorem for {\tt o} 3832may be given 3833equally well as any of the following completely equivalent versions: 3834\pagebreak[2] 3835{\tt \begin{tabbing} 3836$\forall$f g x. (\=f o g) x = \\ 3837\> abs3 (((abs2 --> rep3) f o (abs1 --> rep2) g) (rep1 x)) \\ 3838$\forall$f g. \=f o g = \\ 3839\> (rep1 --> abs3) ((abs2 --> rep3) f o (abs1 --> rep2) g) \\ 3840$\forall$f. \=\$o f = \\ 3841\> ((abs1 --> rep2) --> (rep1 --> abs3)) (\$o ((abs2 --> rep3) f)) \\ 3842\$o = ((abs2 --> rep3) --> (abs1 --> rep2) --> (rep1 --> abs3)) \$o 3843\end{tabbing}} 3844In each of the versions, the type of the {\tt \$o} on the left hand side 3845of the equality 3846is {\tt ('e -> 'f) -> ('d -> 'e) -> ('d -> 'f)}, 3847while the type of the {\tt \$o} on the right hand side 3848is {\tt ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)}. 3849The last version has higher order and lesser arity than the 3850earlier versions. In fact, the four versions above have arities 38513, 2, 1, and 0, respectively. 3852The earlier versions may be easier to understand and prove than the 3853last version. 3854For the quotient package's internal use, all preservation 3855theorems are automatically converted to the lowest order and highest 3856arity possible, and then all higher order versions are produced 3857% The entire collection of versions is 3858and used for lifting theorems 3859which involve the operator. 3860 3861\vfill 3862 3863\begin{table} 3864\begin{center} 3865{\bfseries TABLE 1.\\ 3866Preservation 3867%Definition 3868and Respectfulness Theorems for Polymorphic Operators}\\[1ex] 3869\begin{tabular}{|lll|l|l|} 3870\hline 3871\multicolumn{3}{|l|} 3872{Lifted Operators} & 3873%Lifted 3874Preservation 3875%Definition 3876Theorems & Respectfulness Theorems \\ 3877\hline 3878{\tt $\forall$\_::\_.\_} & $\rightarrow$ & {\tt $\forall$\_.\_} & {\tt FORALL\_PRS} & {\tt RES\_FORALL\_RSP} \\ 3879{\tt $\exists$\_::\_.\_} & $\rightarrow$ & {\tt $\exists$\_.\_} & {\tt EXISTS\_PRS} & {\tt RES\_EXISTS\_RSP} \\ 3880{\tt $\exists !!$\_::\_.\_} & $\rightarrow$ & {\tt $\exists !$\_.\_} 3881& {\tt EXISTS\_UNIQUE\_PRS} & {\tt RES\_EXISTS\_EQUIV\_RSP} \\ 3882% {\tt \verb+\+\_.\_} & & & {\tt LAMBDA\_PRS} & {\tt LAMBDA\_RSP} \\ 3883%{\tt \verb+\+\_::\_.\_} & $\rightarrow$ & {\tt \verb+\+\_.\_} 3884{\tt $\lambda$\_::\_.\_} & $\rightarrow$ & {\tt $\lambda$\_.\_} 3885& {\tt ABSTRACT\_PRS} & {\tt RES\_ABSTRACT\_RSP} \\ 3886{\tt COND} & & & {\tt COND\_PRS} & {\tt COND\_RSP} \\ 3887{\tt LET} & & & {\tt LET\_PRS} & {\tt LET\_RSP} \\ 3888{\tt FST} & & & {\tt FST\_PRS} & {\tt FST\_RSP} \\ 3889{\tt SND} & & & {\tt SND\_PRS} & {\tt SND\_RSP} \\ 3890{\tt ,} & & & {\tt COMMA\_PRS} & {\tt COMMA\_RSP} \\ 3891{\tt CURRY} & & & {\tt CURRY\_PRS} & {\tt CURRY\_RSP} \\ 3892{\tt UNCURRY} & & & {\tt UNCURRY\_PRS} & {\tt UNCURRY\_RSP} \\ 3893{\tt \#\#} & & & {\tt PAIR\_MAP\_PRS} & {\tt PAIR\_MAP\_RSP} \\ 3894{\tt INL} & & & {\tt INL\_PRS} & {\tt INL\_RSP} \\ 3895{\tt INR} & & & {\tt INR\_PRS} & {\tt INR\_RSP} \\ 3896{\tt ISL} & & & {\tt ISL\_PRS} & {\tt ISL\_RSP} \\ 3897{\tt ISR} & & & {\tt ISR\_PRS} & {\tt ISR\_RSP} \\ 3898{\tt ++} & & & {\tt SUM\_MAP\_PRS} & {\tt SUM\_MAP\_RSP} \\ 3899{\tt CONS} & & & {\tt CONS\_PRS} & {\tt CONS\_RSP} \\ 3900{\tt NIL} & & & {\tt NIL\_PRS} & {\tt NIL\_RSP} \\ 3901{\tt MAP} & & & {\tt MAP\_PRS} & {\tt MAP\_RSP} \\ 3902{\tt LENGTH} & & & {\tt LENGTH\_PRS} & {\tt LENGTH\_RSP} \\ 3903{\tt APPEND} & & & {\tt APPEND\_PRS} & {\tt APPEND\_RSP} \\ 3904{\tt FLAT} & & & {\tt FLAT\_PRS} & {\tt FLAT\_RSP} \\ 3905\multicolumn{3}{|l|} 3906{\tt REVERSE} & {\tt REVERSE\_PRS} & {\tt REVERSE\_RSP} \\ 3907{\tt FILTER} & & & {\tt FILTER\_PRS} & {\tt FILTER\_RSP} \\ 3908{\tt NULL} & & & {\tt NULL\_PRS} & {\tt NULL\_RSP} \\ 3909{\tt SOME\_EL} & & & {\tt SOME\_EL\_PRS} & {\tt SOME\_EL\_RSP} \\ 3910{\tt ALL\_EL} & & & {\tt ALL\_EL\_PRS} & {\tt ALL\_EL\_RSP} \\ 3911{\tt FOLDL} & & & {\tt FOLDL\_PRS} & {\tt FOLDL\_RSP} \\ 3912{\tt FOLDR} & & & {\tt FOLDR\_PRS} & {\tt FOLDR\_RSP} \\ 3913{\tt NONE} & & & {\tt NONE\_PRS} & {\tt NONE\_RSP} \\ 3914{\tt SOME} & & & {\tt SOME\_PRS} & {\tt SOME\_RSP} \\ 3915{\tt IS\_SOME} & & & {\tt IS\_SOME\_PRS} & {\tt IS\_SOME\_RSP} \\ 3916{\tt IS\_NONE} & & & {\tt IS\_NONE\_PRS} & {\tt IS\_NONE\_RSP} \\ 3917{\tt OPTION\_MAP} & & & {\tt OPTION\_MAP\_PRS} & {\tt OPTION\_MAP\_RSP} \\ 3918% function application & & & {\tt APPLY\_PRS} & {\tt APPLY\_RSP} \\ 3919%\multicolumn{3}{|l|} 3920%{{\tt I}, {\tt K}, {\tt o}, {\tt C}, {\tt W}} 3921%& {\tt I\_PRS}, {\tt K\_PRS}, {\tt o\_PRS}, etc. \ 3922%& {\tt I\_RSP}, {\tt K\_RSP}, {\tt o\_RSP}, etc. \\ 3923{\tt I} & & & {\tt I\_PRS} & {\tt I\_RSP} \\ 3924{\tt K} & & & {\tt K\_PRS} & {\tt K\_RSP} \\ 3925{\tt o} & & & {\tt o\_PRS} & {\tt o\_RSP} \\ 3926{\tt C} & & & {\tt C\_PRS} & {\tt C\_RSP} \\ 3927{\tt W} & & & {\tt W\_PRS} & {\tt W\_RSP} 3928\begin{comment} 3929{\tt IN} & & & {\tt IN\_PRS} & {\tt IN\_RSP} \\ 3930{\tt EMPTY} & & & {\tt EMPTY\_PRS} & {\tt EMPTY\_RSP} \\ 3931{\tt UNIV} & & & {\tt UNIV\_PRS} & {\tt UNIV\_RSP} \\ 3932\multicolumn{3}{|l|}{{\tt INTER}, {\tt UNION}} 3933 & {\tt INTER\_PRS}, {\tt UNION\_PRS} & {\tt INTER\_RSP}, {\tt UNION\_RSP} \\ 3934%{\tt INTER} & & & {\tt INTER\_PRS} & {\tt INTER\_RSP} \\ 3935%{\tt UNION} & & & {\tt UNION\_PRS} & {\tt UNION\_RSP} \\ 3936{\tt SUBSETR} & $\rightarrow$ & {\tt SUBSET} 3937& {\tt SUBSET\_PRS} & {\tt SUBSETR\_RSP} \\ 3938{\tt PSUBSETR} & $\rightarrow$ & {\tt PSUBSET} 3939& {\tt PSUBSET\_PRS} & {\tt PSUBSETR\_RSP} \\ 3940{\tt IMAGER} & $\rightarrow$ & {\tt IMAGE} 3941& {\tt IMAGE\_PRS} & {\tt IMAGER\_RSP} \\ 3942\end{comment} 3943\\ 3944\hline 3945\end{tabular} 3946\\ 3947\end{center} 3948An arrow 3949({\it lower} $\rightarrow$ {\it higher}) 3950indicates that in 3951preservation theorems, 3952%definition, 3953the lower operator 3954is different 3955%differs 3956from the higher, 3957%otherwise 3958else 3959it 3960%the operator 3961is the same. 3962%\\ 3963Respectfulness theorems concern 3964{\it lower}. 3965%the lower operator. 3966\end{table} 3967 3968% 3969\subsection{Respectfulness of polymorphic functions: {\tt poly\_respects}} 3970% 3971\label{polyrespects} 3972 3973%\item 3974{\tt poly\_respects} is a list of theorems expressing the 3975respectfulness of generic, polymorphic functions. 3976%such as {\tt CONS}, {\tt LENGTH}, {\tt FST}, {\tt I}, or {\tt o}. 3977 3978Since the types of 3979these functions are polymorphic, instances of the functions may be applied 3980to arguments of the types being lifted. 3981%or the higher, lifted types. 3982Each theorem expresses 3983that an operator respects the \quotient{} relations involved, just as 3984for the {\tt respects} field (\S\ref{respectfulness}), 3985except that the theorem conditions 3986the respectfulness of the operator upon the polymorphic types being 3987quotients. The conditioning is the same as that described 3988in the previous section 3989for {\tt poly\_preserves} (\S\ref{polypreserves}). 3990 3991These theorems have the following general form. 3992\begin{center} 3993\begin{tabular}{rl} 3994$\vdash$ 3995& {\tt $\forall$R1 (abs1:$\alpha_1$->$\beta_1$) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$} \\ 3996& {\tt ...} \\ 3997& {\tt $\forall$Rn (absn:$\alpha_n$->$\beta_n$) repn. QUOTIENT Rn absn repn $\Rightarrow$} \\ 3998& {\tt $\forall$(x1:$\gamma_1$) (y1:$\gamma_1$) ... (xk:$\gamma_k$) (yk:$\gamma_k$).} 3999\\ 4000& \hspace{12mm} 4001{\tt $R_1$ x1 y1 \ 4002$\wedge$ \ 4003... \ 4004$\wedge$ \ 4005$R_k$ xk yk $\Rightarrow$ 4006} \\ 4007& \hspace{12mm} 4008{\tt $R_c$ (C x1 ... xk) (C y1 ... yk)} \\ 4009\end{tabular} 4010\end{center} 4011where 4012\begin{enumerate} 4013\item 4014the constant {\tt C} has a polymorphic type with $n$ type variables, 4015$\alpha_1, ..., \alpha_n$, 4016\item 4017$\beta_1, ..., \beta_n$ are $n$ other type variables, 4018% and where 4019\item 4020the type of {\tt C} is of the form 4021{\tt $\gamma_1$ -> ... -> $\gamma_k$ -> $\gamma_c$} \\ 4022({\tt C} is a curried function of $k$ arguments, with a return value of 4023type $\gamma_c$), \\ 4024with 4025all type variables in the $\gamma_1$, ..., $\gamma_k$, $\gamma_c$ types 4026contained within $\alpha_1$,~...,~$\alpha_n$, 4027and 4028\item 4029{\tt $R_i$:$\gamma_i$ -> $\gamma_i$ -> bool} 4030is the (possibly equality, aggregate, or higher-order) 4031\quotient{} relation 4032for the type $\gamma_i$, for all $i=1,...,k,c$. 4033This is an expression, not simply an 4034{\tt Ri} variable. 4035\end{enumerate} 4036 4037For clarity, we will discuss examples for particular polymorphic 4038operators, beginning with simpler ones. In each case, the main driver 4039of the form of the resulting theorem is the operator's type, 4040in particular the number of arguments, the type of each, and the type 4041returned by the operator. 4042 4043\pagebreak[3] 4044The respectfulness theorem for {\tt NIL} is 4045{\tt \begin{tabbing} 4046\hspace{5.5mm} 4047 $\vdash \forall$R\=\ (abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\ 4048\> LIST\_REL R [] [] 4049\end{tabbing}} 4050The operator {\tt NIL} has polymorphic type {\tt ('a)list}. 4051It has one type variable, {\tt 'a}, so $n = 1$. 4052It has no arguments, so $k = 0$. 4053The result type is 4054%$\gamma_c$ = 4055{\tt ('a)list}, 4056%The lifted version of this type is 4057%$\delta_c$ = {\tt ('b)list}. 4058for which 4059the \quotient{} relation 4060%for $\gamma_c$ 4061is {\tt LIST\_REL R}. 4062 4063\pagebreak[2] 4064The respectfulness theorem for {\tt LENGTH} is 4065{\tt \begin{tabbing} 4066\hspace{5.5mm} 4067 $\vdash \forall$R\=\ (abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\ 4068\> $\forall$l1 l2. \=LIST\_REL R l1 l2 $\Rightarrow$ \\ 4069\>\> (LENGTH l1 = LENGTH l2) 4070\end{tabbing}} 4071The operator {\tt LENGTH} has polymorphic type {\tt ('a)list -> num}. 4072It has one type variable, {\tt 'a}, so $n = 1$. 4073It has one argument, so $k = 1$. 4074The argument type is 4075%$\gamma_1$ = 4076{\tt ('a)list}, 4077for which 4078the \quotient{} relation 4079%for $\gamma_1$ 4080is {\tt LIST\_REL R}. 4081The result type is 4082%$\gamma_c$ = 4083{\tt num}, 4084for which 4085the \quotient{} relation 4086%for $\gamma_c$ 4087is {\tt =}. 4088%The lifted versions of these types are 4089%$\delta_1$ = {\tt ('b)list}, 4090%$\delta_c$ = {\tt num}. 4091 4092The respectfulness theorem for {\tt CONS} is 4093{\tt \begin{tabbing} 4094\hspace{5.5mm} 4095 $\vdash \forall$R\=\ (abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\ 4096\> $\forall$t\=1 t2 h1 h2. \\ 4097\>\> R h1 h2 $\wedge$ LIST\_REL R t1 t2 $\Rightarrow$ \\ 4098\>\> LIST\_REL R (h1::t1) (h2::t2) 4099\end{tabbing}} 4100The operator {\tt CONS} has polymorphic type {\tt 'a -> ('a)list -> ('a)list}. 4101It has one type variable, {\tt 'a}, so $n = 1$. 4102It has two arguments, so $k = 2$. 4103The first argument type is 4104%$\gamma_1$ = 4105{\tt 'a}, 4106for which 4107the \quotient{} relation 4108%for $\gamma_1$ 4109is {\tt R}. 4110The second argument type is 4111%$\gamma_2$ = 4112{\tt ('a)list}, 4113for which 4114the \quotient{} relation 4115%for $\gamma_2$ 4116is {\tt LIST\_REL R}. 4117The result type is 4118%$\gamma_c$ = 4119{\tt ('a)list}, 4120for which 4121the \quotient{} relation 4122%for $\gamma_c$ 4123is {\tt LIST\_REL R}. 4124%The lifted versions of these types are 4125%$\delta_1$ = {\tt 'b}, 4126%$\delta_2$ = {\tt ('b)list}, 4127%$\delta_c$ = {\tt ('b)list}. 4128 4129The respectfulness theorem for {\tt FST} is 4130{\tt \begin{tabbing} 4131\hspace{5.5mm} 4132 $\vdash$ \=$\forall$R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\ 4133\> $\forall$R\=2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\ 4134\>\> $\forall$p1 p2. \=(R1 \#\#\# R2) p1 p2 $\Rightarrow$ \\ 4135\>\>\> R1 (FST p1) (FST p2) 4136\end{tabbing}} 4137The operator {\tt FST} has polymorphic type {\tt ('a \# 'b) -> 'a}. 4138It has two type variables, {\tt 'a} and {\tt 'b}, so $n = 2$. 4139It has one argument, so $k = 1$. 4140The argument type is 4141%$\gamma_1$ = 4142{\tt ('a \# 'b)}, 4143for which 4144the \quotient{} relation 4145%for $\gamma_1$ 4146is {\tt R1 \#\#\# R2}. 4147The result type is 4148%$\gamma_c$ = 4149{\tt 'a}, 4150for which 4151the \quotient{} relation 4152%for $\gamma_c$ 4153is {\tt R1}. 4154%The lifted versions of these types are 4155%$\delta_1$ = {\tt ('c \# 'd)}, 4156%$\delta_c$ = {\tt 'c}. 4157 4158The respectfulness theorem for the composition operator {\tt o} is 4159{\tt \begin{tabbing} 4160\hspace{5.5mm} 4161 $\vdash$ \=$\forall$R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\ 4162\> $\forall$R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\ 4163\> $\forall$R\=3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 $\Rightarrow$ \\ 4164\>\> $\forall$f\=1 f2 g1 g2. \\ 4165\>\>\> (R2 ===> R3) f1 f2 $\wedge$ (R1 ===> R2) g1 g2 $\Rightarrow$ \\ 4166\>\>\> (R1 ===> R3) (f1 o g1) (f2 o g2) 4167\end{tabbing}} 4168The operator {\tt o} has type 4169{\tt ('b ->\;'c) -> ('a ->\;'b) -> ('a ->\;'c)}, 4170which is polymorphic and also higher order. 4171It has three type variables, {\tt 'a}, {\tt 'b}, and {\tt 'c}, so $n = 3$. 4172It has two arguments, so $k = 2$. 4173The first argument type is 4174%$\gamma_1$ = 4175{\tt 'b -> 'c}, 4176for which 4177the \quotient{} relation 4178%for $\gamma_1$ 4179is {\tt R2 ===> R3}. 4180The second argument type is 4181%$\gamma_2$ = 4182{\tt 'a -> 'b}, 4183for which 4184the \quotient{} relation 4185%for $\gamma_2$ 4186is {\tt R1 ===> R2}. 4187The result type is 4188%$\gamma_c$ = 4189{\tt 'a -> 'c}, 4190for which 4191the \quotient{} relation 4192%for $\gamma_c$ 4193is {\tt R1 ===> R3}. 4194%The lifted versions of these types are 4195%$\delta_1$ = {\tt 'e -> 'f}, 4196%$\delta_1$ = {\tt 'd -> 'e}, 4197%$\delta_c$ = {\tt 'd -> 'f}. 4198 4199Whenever there are arguments to the constant, there are 4200multiple equivalent ways to state the respectfulness theorem. 4201For example, the respectfulness theorem for {\tt o} may be given 4202equally well with any of the following as the main part, after the 4203{\tt QUOTIENT} conditions: 4204\pagebreak[2] 4205{\tt \begin{tabbing} 4206... $\forall$f\=1 f2 g1 g2 x1 x2. \\ 4207\> (R2\=\ ===> R3) f1 f2 $\wedge$ (R1 ===> R2) g1 g2 $\wedge$ R1 x1 x2 $\Rightarrow$ \\ 4208\>\> R3 ((f1 o g1) x1) ((f2 o g2) x2) \\ 4209... $\forall$f1 f2 g1 g2. (R2 ===> R3) f1 f2 $\wedge$ (R1 ===> R2) g1 g2 $\Rightarrow$ \\ 4210\>\> (R1 ===> R3) (f1 o g1) (f2 o g2) \\ 4211... $\forall$f1 f2. (R2 ===> R3) f1 f2 $\Rightarrow$ \\ 4212\>\> ((R1 ===> R2) ===> (R1 ===> R3)) (\$o f1) (\$o f2) \\ 4213... ((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) \$o \$o 4214\end{tabbing}} 4215The last version has higher order and lesser arity than the 4216earlier versions. In fact, the four versions above have arities 42173, 2, 1, and 0, respectively. 4218Interestingly, the last version contains no variables (outside of the 4219relation variables). 4220The earlier versions may be easier to understand and prove than the 4221last version. For the quotient package's internal use, all respectfulness 4222theorems are automatically converted to the highest order and lowest 4223arity possible, usually with arity zero. 4224 4225A substantial collection of these respectfulness theorems for various 4226standard polymorphic functions of the HOL logic have been proven already and 4227is available in the quotient library theories (see Table 1). 4228If there is a need to use a 4229polymorphic function not covered by these, the corresponding respectfulness 4230theorem can be proven by the user, using the same approach as for the example 4231theorems above, as shown in the theory scripts of the quotient library. 4232 4233 4234% 4235\subsection{Theorems to be lifted: {\tt old\_thms}} 4236% 4237\label{oldtheorem} 4238 4239%\item 4240{\tt old\_thms} are the theorems to be lifted. They should involve only 4241constants (including functions) of the lower, original level, 4242with no mention of any lifted constants or functions. 4243The constants involved must respect 4244the equivalence relations involved, 4245as justified by theorems included 4246in {\tt respects} (see section \ref{respectfulness}) 4247and {\tt poly\_respects} (see section \ref{polyrespects}). 4248The constants must also be either constants being lifted, or else constants 4249preserved by the quotient, as justified by theorems included in 4250{\tt poly\_preserves} (see section \ref{polypreserves}). 4251Each theorem must not have any free variables, and it also must not 4252have any hypotheses, only a conclusion. 4253 4254 4255 4256% 4257\section{Restrictions on lifting of theorems} 4258% 4259\label{restrictions} 4260 4261This section describes the restrictions needed for theorems to lift; 4262the next section relaxes these somewhat, but 4263properly, theorems should obey these restrictions. 4264 4265It is important to remember that even if all the necessary information 4266is provided properly, not all theorems of the lower level 4267can be successfully lifted. 4268 4269To successfully lift, all of the functions a theorem mentions must 4270respect the equivalence relations involved in creating the lifted types. 4271While for the most part properties that are intended to be true at 4272both levels will be expressed in theorems that will lift, there are 4273significant issues that can arise. 4274 4275The first issue is that the normal equality relation ($=$) between elements 4276of a lower type is a function that does not respect the equivalence 4277relation for that type. This means that theorems that mention the 4278equality of elements of the lower type will not in general lift. 4279Usually the statement of the theorem should be revised, 4280with the equivalence relation substituted for the equality relation; 4281this is a different theorem which will in general require its own proof. 4282Then if the lifting is successful, it will lift to 4283a higher version where the equivalence between lower values has been 4284replaced by equality between higher values. 4285%This is entirely consistent with the meaning of the lifting operation. 4286 4287The second issue is that the universal and existential quantification 4288operators 4289%({\tt !}, {\tt ?}, or $\forall$, $\exists$) 4290are not in general respectful. 4291%This has a significant impact, since these operators are so universally used. 4292In particular, quantification over function types 4293may consider functions that are not respectful. 4294For example, in the lambda calculus example, one theorem to be 4295lifted is the induction theorem: 4296{\tt \begin{tabbing} 4297\hspace{5.5mm} 4298 $\vdash \forall$P\=. \\ 4299\> ($\forall$v. P (Var1 v)) $\wedge$ \\ 4300\> ($\forall$t t0. P t $\wedge$ P t0 $\Rightarrow$ P (App1 t t0)) $\wedge$ \\ 4301\> ($\forall$t. P t $\Rightarrow$ $\forall$v. P (Lam1 v t)) $\Rightarrow$ \\ 4302\> ($\forall$t. P t) 4303\end{tabbing}} 4304 4305In this theorem the variable {\tt P} has type {\tt term1 -> bool}. 4306This variable is universally quantified, so all possible functions of 4307this type are considered as possible values of {\tt P}. 4308Unfortunately, some functions of this type do not respect the 4309alpha-equivalence of terms. This respectfulness would be expressed as 4310\begin{center} 4311{\tt $\forall$t1 t2. ALPHA t1 t2 $\Rightarrow$ (P t1 = P t2)} 4312\end{center} 4313But this is not true of all functions 4314of the type {\tt term1 -> bool}. 4315For example, consider the particular function {\tt P1} defined by 4316structural recursion as 4317{\tt \begin{tabbing} 4318\hspace{22.0mm} 4319 \=($\forall$x. \ \ P1 (Var1 x) \ \ = F) $\wedge$ \\ 4320\> ($\forall$t u. P1 (App1 t u) = P1 t $\vee$ P1 u) $\wedge$ \\ 4321\> ($\forall$x u. P1 (Lam1 x u) = P1 u $\vee$ (x = "a")) 4322\end{tabbing}} 4323Then {\tt P1 t} is true if and only if the term {\tt t} contains 4324a subexpression of the form {\tt Lam1 "a" u}, where the bound variable 4325is {\tt "a"}. This {\tt P1} does not satisfy the respectfulness principle 4326since, for example, {\tt ALPHA (Lam1 "a" (Var1 "a")) (Lam1 "b" (Var1 "b"))} 4327but then {\tt P1 (Lam1 "a" (Var1 "a"))} is true while 4328{\tt P1~(Lam1 "b" (Var1 "b"))} is false. 4329 4330The point is that if such non-respectful functions are considered as 4331possible values of {\tt P}, then it becomes impossible to lift the 4332theorem, and in fact in general it would be unsound to do so. 4333The higher version of the theorem will describe quantification over 4334functions of the higher types, and these functions correspond only to 4335respectful functions of the lower types. Non-respectful functions at the 4336lower level have 4337{\bf no} corresponding function at the higher level. So the statement of the 4338theorem needs to be revised to quantify only over functions which are 4339respectful. 4340For the example above, the theorem needs to be 4341rephrased 4342%and reproven 4343as 4344{\tt \begin{tabbing} 4345$\vdash \forall$P\=\ :: respects (ALPHA ===> \$=). \\ 4346\> ($\forall$v. P (Var1 v)) $\wedge$ \\ 4347\> ($\forall$t t0 :: respects ALPHA. P t $\wedge$ P t0 $\Rightarrow$ P (App1 t t0)) $\wedge$ \\ 4348\> ($\forall$t :: respects ALPHA. P t $\Rightarrow$ $\forall$v. P (Lam1 v t)) $\Rightarrow$ \\ 4349\> ($\forall$t :: respects ALPHA. P t) 4350\end{tabbing}} 4351 4352This notation uses the restricted quantifier notation 4353{\tt $\forall${\it x} :: {\it restriction}. {\it body}}, 4354%which is 4355the same as 4356{\tt RES\_FORALL {\it restriction} ($\lambda$x. {\it body})}, 4357introduced in 4358the {\tt res\_quan} library. It also uses the {\tt respects} operator, 4359defined in {\tt quotientTheory} as 4360\begin{center} 4361{\tt respects R (x:'a) = R x x} 4362\end{center} 4363The rephrased induction theorem 4364states that the variable {\tt P} 4365is universally quantified over all functions of type {\tt term1 -> bool} 4366such that those functions respect alpha-equivalence on their domain 4367{\tt term1} 4368(and equality on their range, 4369{\tt bool}), 4370i.e., {\tt respects (ALPHA ===> \$=) P}, which is equal to 4371$$\forall t,t_0 : {\tt term1}.\ 4372{\tt ALPHA}\ t\ t_0 \Rightarrow ({\tt P}\ t = {\tt P}\ t_0).$$ 4373Then the revised version of the induction theorem can be successfully 4374lifted. 4375 4376In general, the {\tt $\forall$} and {\tt $\exists$} 4377operators should be replaced by the 4378{\tt RES\_FORALL} and 4379{\tt RES\_EXISTS} operators, 4380with {\tt respects R} as the restriction, where {\tt R} is the 4381\quotient{} relation for the type being quantified over. 4382This replacement applies even if {\tt R} is simply an equivalence relation, 4383where of course {\tt R x x} always holds by reflexivity, and so 4384no elements of the quantification are excluded. 4385However, when {\tt R} is simple equality, as for types not being lifted, 4386no replacement of {\tt $\forall$} or {\tt $\exists$} 4387is necessary. 4388{\tt RES\_FORALL} and {\tt RES\_EXISTS} can be 4389expressed more conveniently using the 4390``{\tt $\forall$\_::\_.\_}'' and 4391``{\tt $\exists$\_::\_.\_}'' 4392restriction notation, as shown above. 4393%but unfortunately {\tt RES\_EXISTS\_EQUIV} cannot. 4394 4395Finally, on occasion we wish to lift 4396a theorem to create a higher version that contains 4397a unique existance quantifier ($\exists$!). 4398Such a theorem 4399states that for one and only one instance of the quantified variable, 4400a property holds. But that single element at the higher level corresponds 4401to an entire equivalence class of elements at the lower level. 4402To lift some lower theorem to such a statement, 4403the lower theorem must state that the property holds just and only 4404for elements of that equivalence class, rather than for some single element. 4405Therefore one cannot simply lift from 4406a lower version of $\exists$! to a higher version of $\exists$!. Instead, we 4407must introduce a new operator, {\tt RES\_EXISTS\_EQUIV} of type 4408{\tt ('a -> 'a -> bool) -> ('a -> bool) -> bool}. 4409{\tt \begin{tabbing} 4410\hspace{20mm} 4411 RES\=\_EXISTS\_EQUIV R P = \\ 4412\> ($\exists$x::respects R. P x) $\wedge$ \\ 4413\> ($\forall$x y::respects R. P x $\wedge$ P y $\Rightarrow$ R x y) 4414\end{tabbing}} 4415The first argument {\tt R} is the \quotient{} relation for 4416the type being quantified over, 4417and the second argument {\tt P} is the predicate 4418which is being stated as true for some element of that type 4419which respects {\tt R}. 4420%The meaning of 4421{\tt RES\_EXISTS\_EQUIV R P} means that there exist 4422some elements which are respectful of {\tt R} and which satisfy {\tt P}, 4423%and all elements which are respectful of {\tt R} and which satisfy {\tt P} 4424and all such elements 4425are equivalent according to {\tt R}. 4426 4427For convenience, {\tt RES\_EXISTS\_EQUIV} can also be represented using a 4428new restricted quantification binder, $\exists$!!. The parser will translate 4429{\tt $\exists !!$x::R. P x} into {\tt RES\_EXISTS\_EQUIV R ($\lambda$x. P x)}, 4430and the prettyprinter will reverse this. 4431In order to use this notation, in each HOL session 4432one must first execute 4433\begin{verbatim} 4434val _ = associate_restriction ("?!!", "RES_EXISTS_EQUIV"); 4435\end{verbatim} 4436 4437When attempting to lift a theorem, 4438all instances of quantifying by $\exists$! over types being lifted 4439should be replaced by instances of $\exists$!! ({\tt RES\_EXISTS\_EQUIV}) 4440along with the appropriate \quotient{} relation. 4441%and the revised theorem proven before attempting lifting to the higher level. 4442Instances of quantifying by $\exists$! over types not being lifted need 4443not be modified at all. 4444Note that where the restricted quantifier versions of $\forall$ and $\exists$ 4445use restrictions of the form {\tt respects~R}, the restricted quantifier 4446version of $\exists$!! uses just {\tt R} as the restriction. 4447 4448For example, this arises naturally in 4449the function existence theorem proposed by Gordon and 4450Melham for the lambda calculus 4451\cite{GoMe96}: 4452\pagebreak[2] 4453{\tt \begin{tabbing} 4454\hspace{2.5mm} 4455 $\vdash \forall$v\=ar app abs. \\ 4456\> $\exists !$\=hom. \\ 4457\>\> ($\forall$x. hom (Var x) = var x) $\wedge$ \\ 4458\>\> ($\forall$t u. hom (App t u) = app (hom t) (hom u)) $\wedge$ \\ 4459\>\> ($\forall$x u. hom (Lam x u) = abs ($\lambda$y. hom (u <[ [(x,Var y)]))) 4460\end{tabbing}} 4461 4462\noindent 4463To create the above theorem, we need to prove 4464the proper lower version 4465%at the lower level 4466{\tt \begin{tabbing} 4467\hspace{2.5mm} 4468 $\vdash \forall$v\=ar app abs. \\ 4469\> $\exists !!$\=hom :: (ALPHA ===> \$=). \\ 4470\>\> ($\forall$x. hom (Var1 x) = var x) $\wedge$ \\ 4471\>\> ($\forall$t\=\ u :: respects ALPHA. \\ 4472\>\>\> hom (App1 t u) = app (hom t) (hom u)) $\wedge$ \\ 4473\>\> ($\forall$x (u :: respects ALPHA). \\ 4474\>\>\> hom (Lam1 x u) = abs ($\lambda$y. hom (u <[ [(x,Var1 y)]))) 4475\end{tabbing}} 4476\noindent 4477which will then lift. 4478 4479 4480\begin{comment} 4481 4482Only those properties which respect 4483the equivalence relations of the quotient operations will properly lift. 4484An property which would not lift would be one which 4485depended on specific information as to which element of an equivalence 4486class was being referred to. 4487Some theorems describe 4488properties which have no direct corresponding theorem at the abstract, 4489lifted level. Other theorems may have such a corresponding theorem, 4490but they may not be strong enough to infer the lifted theorem. 4491 4492For example, consider the quotient of the non-negative integers 4493by the equivalence 4494relation $\sim$ where $n \sim m$ if and only if $n$ and $m$ are either both 4495even or both odd. This creates two equivalence classes, which are the 4496set of even integers and the set of odd integers. This specifies a new, 4497lifted type with two values for which we can define the constants, 4498{\tt EVEN} as the lifted version of {\tt 0} and {\tt ODD} 4499as the lifted version of {\tt 1}. 4500 4501At the lower level, we can prove the theorem {\tt $\vdash$ \verb+~+(3 = 5)}. 4502But this theorem does not lift to the abstract level, where it would be 4503{\tt $\vdash$ \verb+~+(ODD = ODD)}, which is obviously false. 4504So not every theorem should or will lift! 4505 4506At the lower level, we can prove the theorem {\tt $\vdash$ \verb+~+(0 = 1)}. 4507For this theorem, there {\it is\/} 4508a corresponding theorem at the abstract level, 4509{\tt $\vdash$ \verb+~+(EVEN = ODD)}, which should be true. However, there is just not 4510enough information in the lower theorem {\tt $\vdash$ \verb+~+(0 = 1)} 4511to prove the lifted version, because the lower theorem 4512only states an inequality. What is actually needed is 4513{\tt $\vdash$ \verb+~+(0 $\sim$ 1)}, which states that the two values are 4514not equivalent, which is stronger. 4515{\tt $\vdash$ \verb+~+(0 $\sim$ 1)} implies that 4516{\tt $\vdash$ \verb+~+(0 = 1)}, 4517but not the reverse. 4518{\tt $\vdash$ \verb+~+(0 $\sim$ 1)} is provable at the lower level, 4519and it will successfully lift to {\tt $\vdash$ \verb+~+(EVEN = ODD)}. 4520 4521In general, a property which will lift may be composed only of 4522functions which respect the equivalence relations involved. 4523This includes ordinary equality! 4524But an essential problem here is that the equality operation 4525does not respect the equivalence relation, that is, 4526$$a_1 \sim a_2 \ \wedge \ b_1 \sim b_2 \ \not\Rightarrow \ 4527 (a_1 = b_1 \ \Leftrightarrow \ a_2 = b_2).$$ 4528An instance of this would be that $3 \sim 3$ and $3 \sim 5$, but then 4529$3 = 3$ is true while $3 = 5$ is false. 4530 4531Generally, any mention of equality between elements of a type being 4532lifted will make a theorem not liftable. A variant of the theorem 4533should be proven which substitutes equivalence for the equality. 4534% 4535This should really not be surprising, since the purpose of collapsing 4536equivalence classes into single entities is meant to render the results 4537indistinguishable. Therefore properties which rely on those distinctions 4538will not translate to the higher level, which in particular excludes 4539the equality relation between values which are now being declared as 4540equivalent. 4541 4542\end{comment} 4543 4544%\end{enumerate} 4545 4546% 4547\section{Support for non-standard lifting} 4548% 4549\label{nonstandard} 4550 4551The {\tt define\_quotient\_types} tool 4552for lifting theorems is actually less 4553demanding and more forgiving than has been described up to this point. 4554Automation has been added to recognize several common 4555situations of theorems which may not be in the proper form, but are 4556strong enough to imply the proper form. These are quietly converted 4557and then lifted. 4558 4559Despite the objections to the use of equality 4560in theorems to be lifted mentioned above, in practice equality is commonly used. 4561Many theorems to be lifted have the form 4562{\tt $\vdash$ a = b}, for some expressions {\tt a} and {\tt b} whose type is 4563being lifted. 4564In fact, 4565if $\sim$ is an equivalence relation, 4566this equality implies {\tt $\vdash$ a $\sim$ b}. 4567The tool recognizes this common case and automatically proves 4568the needed revised 4569theorem that only mentions equivalence instead of equality. 4570This can then be lifted. 4571 4572Similarly, theorems of the form {\tt $\vdash$ P $\Rightarrow$ (a = b)}, or even more 4573general examples, can also be 4574automatically revised and then lifted. 4575 4576Universal or existential restricted quantification, where the 4577restriction is of the form {\tt respects R}, for {\tt R} an equivalence 4578relation, do not actually restrict any elements from the quantification. 4579Thus these are really equal to the original ordinary quantification, 4580and the tool is able to create and prove the version with such 4581restricted quantifications from a user-supplied theorem with normal 4582quantification in those places. 4583 4584In addition, theorems which are universal quantifications 4585%with that quantification 4586at the outer level of the theorem, may 4587imply the restricted universal quantifications (their proper form) 4588%using restricted quantification 4589over respectful values. 4590The proper form is automatically proven and then lifted. 4591For example, the tool can lift the 4592lambda calculus induction theorem given earlier without the user first 4593converting it to proper form. 4594 4595Finally, theorems which involve unique existance 4596quantification $\exists$! restricted over functions which are respectful, 4597may imply the corresponding theorem using the 4598restricted $\exists$!! 4599%{\tt RES\_EXISTS\_EQUIV} 4600operator. For example, in the lambda 4601calculus example, we have proven 4602%it is possible to prove 4603at the lower level 4604{\tt \begin{tabbing} 4605 $\vdash \forall$v\=ar app abs. \\ 4606\> $\exists !$\=hom :: respects (ALPHA ===> \$=). \\ 4607\>\> ($\forall$x. hom (Var1 x) = var x) $\wedge$ \\ 4608\>\> ($\forall$t u. hom (App1 t u) = app (hom t) (hom u)) $\wedge$ \\ 4609\>\> ($\forall$x u. hom (Lam1 x u) = abs ($\lambda$y. hom (u <[ [(x,Var1 y)]))) 4610\end{tabbing}} 4611 4612\noindent 4613The tool will first automatically prove the proper version: 4614{\tt \begin{tabbing} 4615 $\vdash \forall$v\=ar app abs. \\ 4616\> $\exists !!$\=hom :: ALPHA ===> \$=. \\ 4617\>\> ($\forall$x. hom (Var1 x) = var x) $\wedge$ \\ 4618\>\> ($\forall$t\=\ u :: respects ALPHA. \\ 4619\>\>\> hom (App1 t u) = app (hom t) (hom u)) $\wedge$ \\ 4620\>\> ($\forall$x (u :: respects ALPHA). \\ 4621\>\>\> hom (Lam1 x u) = abs ($\lambda$y. hom (u <[ [(x,Var1 y)]))) 4622\end{tabbing}} 4623 4624\noindent 4625and then lift the proper version to the desired higher version of this theorem: 4626{\tt \begin{tabbing} 4627 $\vdash \forall$v\=ar app abs. \\ 4628\> $\exists !$\=hom. \\ 4629\>\> ($\forall$x. hom (Var x) = var x) $\wedge$ \\ 4630\>\> ($\forall$t u. hom (App t u) = app (hom t) (hom u)) $\wedge$ \\ 4631\>\> ($\forall$x u. hom (Lam x u) = abs ($\lambda$y. hom (u <[ [(x,Var y)]))) 4632\end{tabbing}} 4633 4634In general, of course, this revising may not work. 4635If the tool cannot automatically prove the proper version from the theorem 4636it is given, it will print out an error message showing the needed revised 4637proper form. The user should prove the proper version manually 4638and then submit 4639it 4640%the proper theorem 4641to the tool for lifting. 4642 4643Finally, we would like to describe some possible reasons to consider 4644when theorems do not lift, apart from improper form as above. First, 4645every constant mentioned in the theorem that takes or returns values 4646of types being lifted must be described in a respectfulness theorem, 4647whether in the {\tt respects} or {\tt poly\_respects} arguments. 4648Also, every such constant in the theorem 4649must be either one being lifted to a new constant in the {\tt defs} argument, 4650or described in a preservation theorem in the {\tt poly\_preserves} argument. 4651Every partial equivalence relation mentioned in any of these theorems 4652should be either one of those mentioned in the {\tt types} argument, 4653or an extension of these, 4654using the relation operators mentioned in sections 4655\ref{equivalence} and 4656\ref{quotientrelation}. 4657If the type of any constant in any theorem 4658involves type operators, like lists or functions, then the associated 4659quotient extension theorems must be provided in the 4660{\tt tyop\_quotients} argument. 4661%except for {\tt FUN\_QUOTIENT}, which is builtin by default. 4662Likewise, the equivalence extension theorems (if available), 4663and the associated relation and map function simplification theorems 4664should be provided 4665in the {\tt tyop\_equivs} and {\tt tyop\_simps} arguments. 4666The error message associated with the exception thrown may help localize 4667the error. 4668The process of the quotient operation may be observed in more detail 4669by setting the variable {\tt quotient.chatting := true}. 4670Lastly, during development it may be more convenient to use the 4671{\tt define\_quotient\_types\_rule} tool, so that the {\tt LIFT\_RULE} 4672function it returns may be applied to candidate lower theorems individually 4673and repeatedly. This helps to retry lifting a troublesome theorem 4674in isolation until it successfully lifts. 4675 4676 4677% 4678\section{Lifting Sets} 4679% 4680\label{liftingsets} 4681 4682The facilities provided so far for higher order quotients are flexible 4683and extensible for the addition of support for new type operators, with 4684their own associated quotient extension theorems, simplification theorems, 4685perhaps equivalence extension theorems, and respectfulness and 4686preservation theorems for the 4687constants associated with the type operator. 4688 4689One commonly used type is sets, which are implemented in the Higher 4690Order Logic theorem prover through the library {\tt pred\_set}. No actual 4691new type is used here, but sets are represented by the function type 4692{\tt 'a -> bool}, where {\tt 'a} is the underlying type of the elements 4693of the set. 4694In fact, there is a close identity between a set and its characteristic 4695function. Nevertheless, it is helpful and intuitive at times to think 4696of sets as sets, not functions, and many normal set operators, such 4697as {\tt INSERT}, {\tt SUBSET}, and {\tt UNION}, are provided. 4698 4699For this type of sets, 4700if the partial equivalence relation 4701on the underlying type is $R$, then 4702the extension of $R$ 4703to the set type is 4704$R \ \mbox{\tt ===>} \ (\mbox{\tt \$=:bool->bool->bool})$. 4705Essentially, sets behave as a specialization of the 4706function quotient extension theorem, where the domain is the base type of $R$ 4707and the range is {\tt bool}, as in 4708{\tt \begin{tabbing} 4709SET\=\_QUOTIENT: \\ 4710\> $\vdash$ \=$\forall R\;$\=${\it abs}\;{\it rep}.\ 4711 \langle R,{\it abs},{\it rep} \rangle \Rightarrow 4712 \langle R\;\mbox{\tt ===>}\;\mbox{\tt \$=},\ 4713 {\it rep}\;\mbox{\tt -->}\;{\tt I},\ 4714 {\it abs}\;\mbox{\tt -->}\;{\tt I} 4715 \rangle$ 4716\end{tabbing}} 4717The associated abstraction function 4718is ${\it rep}\;\mbox{\tt -->}\;{\tt I}$, 4719and the associated representation function 4720is ${\it abs}\;\mbox{\tt -->}\;{\tt I}$. 4721Note that the use of $abs$ vs. $rep$ is counterintuitive. 4722 4723When lifting theorems that contain instances of polymorphic set operators 4724applied to values of types being lifted, some of the normal set 4725operators are preserved across the quotient operation, but several are 4726not. For these operators, we have provided new, similar operators 4727which take into account the partial equivalence relation(s) involved, 4728and thus do successfully lift to their normal set operator counterpart. 4729 4730For example, for the set operator {\tt DIFF}, no problems arise, and 4731we can prove its respectfulness and preservation theorems of the normal 4732form. 4733 4734{\tt \begin{tabbing} 4735DIFF\_PRS: \\ 4736\hspace{5.5mm} 4737 $\vdash$ \=$\forall$R \=(abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\ 4738\>\> $\forall$s t. \=s DIFF t = \\ 4739\>\>\> (rep --> I) (((abs --> I) s) DIFF ((abs --> I) t)) \\ 4740\\ 4741DIFF\_RSP: \\ 4742\hspace{5.5mm} 4743 $\vdash$ $\forall$R (abs:'a -> 'b) rep. QUOTIENT R abs rep $\Rightarrow$ \\ 4744\>\> $\forall$s1 s2 t1 t2. \\ 4745\>\>\> (R ===> \$=) s1 s2 $\wedge$ (R ===> \$=) t1 t2 $\Rightarrow$ \\ 4746\>\>\> (R ===> \$=) (s1 DIFF t1) (s2 DIFF t2) 4747\end{tabbing}} 4748 4749But the following operators are {\it not\/} preserved, and have the indicated 4750associated ``regular'' versions: 4751 4752\begin{center} 4753{\tt \begin{tabular}{|c|c|} 4754\hline 4755{\rm Normal} & {\rm Regular} \\ 4756\hline 4757INSERT & INSERTR \\ 4758DELETE & DELETER \\ 4759SUBSET & SUBSETR \\ 4760PSUBSET & PSUBSETR \\ 4761\ DISJOINT \ & \ DISJOINTR \ \\ 4762FINITE & FINITER \\ 4763GSPEC & GSPECR \\ 4764IMAGE & IMAGER \\ 4765\hline 4766\end{tabular}} 4767\end{center} 4768 4769Even if the original operator is infix, all of the new operators 4770are prefix operators, to ease the addition of the new arguments. 4771 4772Most of these regular operators take one new argument, which is the 4773partial equivalence relation of the underlying type of the set. 4774For {\tt GSPECR} and {\tt IMAGER}, there are two new arguments, 4775which are the partial equivalence relations of 4776the types used for the polymorphic type variables of the original 4777{\tt GSPEC} or {\tt IMAGE}. To make this clearer, here are the 4778preservation theorems for these two operators. 4779 4780{\tt \begin{tabbing} 4781GSPEC\_PRS: \\ 4782\hspace{1.5mm} 4783 $\vdash$ \=$\forall$R\=1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\ 4784\> $\forall$R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\ 4785\>\> $\forall$f. \=GSPEC f = \\ 4786\>\>\> (rep2 --> I) (GSPECR R1 R2 ((abs1 --> (rep2 \#\# I)) f)) \\ 4787\\ 4788IMAGE\_PRS: \\ 4789\hspace{1.5mm} 4790 $\vdash$ $\forall$R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 $\Rightarrow$ \\ 4791\> $\forall$R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 $\Rightarrow$ \\ 4792\>\> $\forall$f s. IMAGE f s = \\ 4793\>\>\> (rep2 --> I) (IMAGER R1 R2 \=((abs1 --> rep2) f) \\ 4794\>\>\>\> ((abs1 --> I) s)) 4795\end{tabbing}} 4796 4797The polymorphic preservation and respectfulness theorems for all these 4798operators are found in {\tt quotient\_pred\_setTheory}, where e.g. the 4799names of these theorems for the {\tt INSERT} operator are 4800{\tt INSERT\_PRS} and {\tt INSERTR\_RSP}, respectively. 4801 4802To ease the process of formulating the appropriate regular version of a 4803theorem that a user wishes to lift, the tools will examine a given 4804theorem to see if it is regular, and if not, will construct a regular 4805version which if proved by the user will (hopefully) lift. 4806Here are some examples. 4807 4808{\tt \begin{tabbing} 4809val \=LIFT\_RULE = \\ 4810\> define\_quotient\_types\_full\_rule \\ 4811\> \{types = [\{name = "term", equiv = ALPHA\_EQUIV\}], \\ 4812\> \ defs = fnlist, \\ 4813\> \ tyop\_equivs = [], \\ 4814\> \ tyop\_quotients = [], \\ 4815\> \ tyop\_simps = [], \\ 4816\> \ respects = respects, \\ 4817\> \ poly\_preserves = [\=IN\_PRS,EMPTY\_PRS,UNIV\_PRS,UNION\_PRS, \\ 4818\>\> INTER\_PRS,SUBSET\_PRS,PSUBSET\_PRS, \\ 4819\>\> DELETE\_PRS,INSERT\_PRS,DIFF\_PRS,GSPEC\_PRS, \\ 4820\>\> DISJOINT\_PRS,FINITE\_PRS,IMAGE\_PRS], \\ 4821\> \ poly\_respects \ = [IN\_RSP,EMPTY\_RSP,UNIV\_RSP,UNION\_RSP, \\ 4822\>\> INTER\_RSP,SUBSETR\_RSP,PSUBSETR\_RSP, \\ 4823\>\> DELETER\_RSP,INSERTR\_RSP,DIFF\_RSP,GSPECR\_RSP, \\ 4824\>\> DISJOINTR\_RSP,FINITER\_RSP,IMAGER\_RSP], \\ 4825 \\ 4826- LIFT\_RULE (INST\_TYPE [alpha |-> ``:'a term1``] EXTENSION) \\ 4827\ \ handle e => Raise e; \\ 4828 \\ 4829Exception raised at quotient.REGULARIZE: \\ 4830Could not lift the irregular theorem \\ 4831$\vdash$ $\forall$s t. (s = t) $\Leftrightarrow$ $\forall$x. x IN s $\Leftrightarrow$ x IN t \\ 4832May try proving and then lifting \\ 4833$\forall$s t::respects (ALPHA ===> \$=). \\ 4834\ \ (ALPHA ===> \$=) s t $\Leftrightarrow$ $\forall$x::respects ALPHA. x IN s $\Leftrightarrow$ x IN t \\ 4835! Uncaught exception: \\ 4836! HOL\_ERR \\ 4837 \\ 4838- LIFT\_RULE (INST\_TYPE [alpha |-> ``:'a term1``] SUBSET\_TRANS) \\ 4839\ \ handle e => Raise e; \\ 4840 \\ 4841Exception raised at quotient.REGULARIZE: \\ 4842Could not lift the irregular theorem \\ 4843$\vdash$ $\forall$s t u. s SUBSET t $\wedge$ t SUBSET u $\Rightarrow$ s SUBSET u \\ 4844May try proving and then lifting \\ 4845$\forall$s t u::respects (ALPHA ===> \$=). \\ 4846\ \ SUBSETR ALPHA s t $\wedge$ SUBSETR ALPHA t u $\Rightarrow$ SUBSETR ALPHA s u \\ 4847! Uncaught exception: \\ 4848! HOL\_ERR \\ 4849 \\ 4850- LIFT\_RULE \\ 4851\ \ \ \ (INST\_TYPE [alpha |-> ``:'a term1``, beta |-> ``:'b term1``] \\ 4852\ \ \ \ \ \ INJECTIVE\_IMAGE\_FINITE); \\ 4853 \\ 4854Exception raised at quotient.REGULARIZE: \\ 4855Could not lift the irregular theorem \\ 4856$\vdash$ $\forall$f. 4857 ($\forall$x y. (f x = f y) $\Leftrightarrow$ (x = y)) $\Rightarrow$ \\ 4858\ \ \ \ \ \ $\forall$s. FINITE (IMAGE f s) $\Leftrightarrow$ FINITE s \\ 4859May try proving and then lifting \\ 4860$\forall$f::respects (ALPHA ===> ALPHA). \\ 4861\ \ ($\forall$x y::respects ALPHA. ALPHA (f x) (f y) $\Leftrightarrow$ ALPHA x y) $\Rightarrow$ \\ 4862\ \ \ $\forall$s::respects (ALPHA ===> \$=). \\ 4863\ \ \ \ \ FINITER ALPHA (IMAGER ALPHA ALPHA f s) $\Leftrightarrow$ FINITER ALPHA s \\ 4864! Uncaught exception: \\ 4865! HOL\_ERR 4866\end{tabbing}} 4867 4868In each case the suggested regular version of the theorem can be 4869copied from the error message, 4870proven by hand, and then submitted to the tool for lifting. 4871 4872Here are the names of the preservation and respectfulness theorems 4873for polymorphic set operators provided in the quotient library. 4874 4875\begin{table} 4876\begin{center} 4877{\bfseries TABLE 2.\\ 4878Preservation 4879%Definition 4880and Respectfulness Theorems for Polymorphic Set Operators}\\[1ex] 4881\begin{tabular}{|lll|l|l|} 4882\hline 4883\multicolumn{3}{|l|} 4884{Lifted Operators} & 4885%Lifted 4886Preservation 4887%Definition 4888Theorems & Respectfulness Theorems \\ 4889\hline 4890{\tt IN} & & & {\tt IN\_PRS} & {\tt IN\_RSP} \\ 4891{\tt EMPTY} & & & {\tt EMPTY\_PRS} & {\tt EMPTY\_RSP} \\ 4892{\tt UNIV} & & & {\tt UNIV\_PRS} & {\tt UNIV\_RSP} \\ 4893{\tt INTER} & & & {\tt INTER\_PRS} & {\tt INTER\_RSP} \\ 4894{\tt UNION} & & & {\tt UNION\_PRS} & {\tt UNION\_RSP} \\ 4895{\tt DIFF} & & & {\tt DIFF\_PRS} & {\tt DIFF\_RSP} \\ 4896{\tt INSERTR} & $\rightarrow$ & {\tt INSERT} 4897& {\tt INSERT\_PRS} & {\tt INSERTR\_RSP} \\ 4898{\tt DELETER} & $\rightarrow$ & {\tt DELETE} 4899& {\tt DELETE\_PRS} & {\tt DELETER\_RSP} \\ 4900{\tt DISJOINTR} & $\rightarrow$ & {\tt DISJOINT} 4901& {\tt DISJOINT\_PRS} & {\tt DISJOINTR\_RSP} \\ 4902{\tt GSPECR} & $\rightarrow$ & {\tt GSPEC} 4903& {\tt GSPEC\_PRS} & {\tt GSPECR\_RSP} \\ 4904{\tt SUBSETR} & $\rightarrow$ & {\tt SUBSET} 4905& {\tt SUBSET\_PRS} & {\tt SUBSETR\_RSP} \\ 4906{\tt PSUBSETR} & $\rightarrow$ & {\tt PSUBSET} 4907& {\tt PSUBSET\_PRS} & {\tt PSUBSETR\_RSP} \\ 4908{\tt FINITER} & $\rightarrow$ & {\tt FINITE} 4909& {\tt FINITE\_PRS} & {\tt FINITER\_RSP} \\ 4910{\tt IMAGER} & $\rightarrow$ & {\tt IMAGE} 4911& {\tt IMAGE\_PRS} & {\tt IMAGER\_RSP} \\ 4912\hline 4913\end{tabular} 4914\\ 4915\end{center} 4916An arrow 4917({\it lower} $\rightarrow$ {\it higher}) 4918indicates that in 4919preservation theorems, 4920%definition, 4921the lower operator 4922is different 4923%differs 4924from the higher, 4925%otherwise 4926else 4927it 4928%the operator 4929is the same. 4930%\\ 4931Respectfulness theorems concern 4932{\it lower}. 4933%the lower operator. 4934\end{table} 4935 4936In addition, several related theorems are provided, including the 4937definitions of the new operators and some of their interactions with other 4938set operators. 4939 4940\pagebreak[4] 4941{\tt \begin{tabbing} 4942IN\_INSERTR: \\ 4943\hspace{5.5mm} 4944\=$\vdash$ $\forall$R\= x s y. y IN INSERTR R x s $\Leftrightarrow$ R y x $\vee$ y IN s \\ 4945IN\_DELETER: \\ 4946\>$\vdash$ $\forall$R s x y. y IN DELETER R s x $\Leftrightarrow$ y IN s $\wedge$ \verb+~+R x y \\ 4947IN\_GSPECR: \\ 4948\>$\vdash$ $\forall$R1 R2 f v. \\ 4949\>\> v IN GSPECR R1 R2 f $\Leftrightarrow$ \\ 4950\>\> $\exists$x::respects R1. (R2 \#\#\# \$=) (v,T) (f x) \\ 4951IN\_IMAGER: \\ 4952\>$\vdash$ $\forall$R1 R2 y f s. \\ 4953\>\> y IN IMAGER R1 R2 f s $\Leftrightarrow$ \\ 4954\>\> $\exists$x::respects R1. R2 y (f x) $\wedge$ x IN s 4955%FINITER\_def: \\ 4956%\> $\vdash$ $\forall$R s. 4957% FINITER R s $\Leftrightarrow$ \\ 4958%\>\> !P\=::respects ((R ===> \$=) ===> \$=). \\ 4959%\>\>\> P \{\} $\wedge$ 4960% ($\forall$s\=::respects (R ===> \$=). \\ 4961%\>\>\>\> P s ==> $\forall$e::respects R. P (INSERTR R e s)) $\Rightarrow$ \\ 4962%\>\>\> P s 4963\end{tabbing}} 4964 4965These facilities for set operators are presented to be helpful, 4966but they are in 4967%a state of 4968development, and should be considered 4969experimental and subject to change. 4970%They will probably change somewhat in future versions. 4971 4972%\vspace{0.7in} 4973 4974 4975% 4976\section{The Sigma Calculus} 4977% 4978\label{sigmacalculus} 4979 4980The untyped sigma calculus was introduced by Abadi and Cardelli in 4981{\it A Theory of Objects} \cite{AbCa96}. 4982It highlights the concept of objects, 4983rather than functions. 4984%including the ideas of messages, methods, arguments to methods, 4985%and replacing an existing method in an object by another. 4986 4987We will use the sigma calculus as an example to demonstrate the quotient 4988package tools. 4989We will first define an initial or ``pre-''version of the 4990language syntax, 4991and then create the refined or ``pure'' version 4992by performing a quotient operation on the initial version. 4993 4994The pre-sigma calculus contains terms denoting objects and methods. 4995We define the sets of object terms $O_1$ and method terms $M_1$ inductively as 4996 4997(1) $x \in O_1$ for all variables $x$; 4998 4999(2) $m_1, \ldots,\, m_n \in M_1 \,\Rightarrow\, 5000 [ l_1 \mathbin{=} m_1,\,\ldots,\,l_n \mathbin{=} m_n ] \in O_1$ 5001 for all labels $l_1,\ldots,\,l_n$; 5002 5003(3) $a \in O_1 \ \Rightarrow \ a.l \in O_1$ for all labels $l$; 5004 5005(4) $a \in O_1 \ \wedge \ m \in M_1 \ \Rightarrow \ 5006 a.l \Lleftarrow m \in O_1$ for all labels $l$; 5007 5008(5) $a \in O_1 \ \Rightarrow \ \varsigma(x)a \in M_1$ for all varibles $x$. 5009 5010$[ l_1 \mathbin{=} m_1, \,\ldots,\, l_n \mathbin{=} m_n ]$ denotes a 5011{\it method dictionary,} 5012as a finite list of {\it entries}, each $l_i \mathbin{=} m_i$ 5013consisting of a label and a method. 5014There should be no duplicates among the labels, but if there are, the first 5015one takes precedence. 5016 5017The form $a.l$ denotes the invocation of the method labelled $l$ in the 5018object $a$. The form $a.l \Lleftarrow m$ denotes the update of the object 5019$a$, where the method labelled $l$ (if any) is replaced by the new 5020method $m$. The form $\varsigma(x)a$ denotes a method with one formal 5021parameter, $x$, and a body $a$. $\varsigma$ is a binder, like $\lambda$ 5022in the lambda calculus. $x$ is a bound variable, 5023and the scope of $x$ is the body $a$. 5024In this scope, $x$ represents the ``self'' parameter, 5025%that is, 5026the object itself which contains this method. 5027%Thus in the sigma calculus 5028%there are no other arguments sent with a message other than simply the 5029%label itself. 5030 5031Given the pre-sigma calculus, we define the pure sigma 5032calculus by identifying object and method terms which are alpha-equivalent 5033\cite{Bar81}. 5034Thus in the pure sigma calculus, $\varsigma(x)x.l_1 = \varsigma(y)y.l_1$, 5035$[l_1 \mathbin{=} \varsigma(x)x] = [l_1 \mathbin{=} \varsigma(y)y]$, et cetera. 5036This is accomplished 5037by forming the quotients of the types of pre-sigma calculus 5038object and method terms by their 5039alpha-equivalence relations. 5040Thus $O = O_1 / {\equiv}_{\alpha}^o$ 5041and $M = M_1 / {\equiv}_{\alpha}^m$, 5042where ${\equiv}_{\alpha}^o$ and ${\equiv}_{\alpha}^m$ are the 5043respective alpha-equivalence relations. 5044 5045%For more on the syntax and semantics of the sigma calculus, with 5046%examples, please see 5047%\cite{AbCa96}. 5048 5049%As an example of a programming language, it is 5050%interesting that the sigma calculus is mutually recursive in 5051%its definition. This is easily seen by noting that $O_1$ is defined in 5052%terms of $M_1$, and vice versa. However, the recursive structure is 5053%actually more deep than might at first appear. The list structure 5054%that is appealed to in the dictionary form is itself a recursively 5055%defined structure, and this introduces its own complexities, as we 5056%shall see later. 5057%It is possible to create a de-Bruin-style representation of the 5058%sigma calculus which has only one type, as done by Sidi O. Ehmety, 5059%but for a name-carrying syntax, mutual recursion is natural. 5060%The mutual recursion inherent in these 5061%fundamental definitions of the syntax 5062%has profound implications for all formal studies of this system. 5063 5064% 5065\section{The Pre-Sigma Calculus in HOL} 5066% 5067\label{presigmacalculus} 5068 5069HOL supports the definition of new nested mutually recursive types 5070by the {\tt Hol\_datatype} function in the 5071{\tt bossLib} library. 5072%(HOL System Description Manual, section 5.2.1). 5073%as described in section 5.2.1 of the HOL System Description Manual. 5074 5075%In addition to defining new types, this tool also defines the 5076%constructor functions for the various cases of how values of the types 5077%may be constructed, and proves several theorems about the interrelationships 5078%of these types and 5079%%constructor 5080%functions. 5081%%This includes the existence of primitive recursive functions on these 5082%%new types, a structural induction principle, the distinctiveness and 5083%%one-to-one properties of the constructors, and a cases theorem. 5084 5085%All of the type definition, constructor function definition, and 5086%subsequent proofs of the above properties is done completely securely, 5087%as a definitional extension of the HOL logic. 5088%This is an 5089%excellent example of appropriate automation, where a terse but powerful 5090%description is completely automatically processed to yield effective and 5091%nontrivial results. 5092 5093%We illustrate the use of this tool with the example mentioned. 5094The syntax 5095of the pre-sigma calculus 5096is defined as follows. 5097 5098\begin{verbatim} 5099val _ = Hol_datatype 5100 5101 (* obj1 ::= x | [li=mi] i in 1..n | a.l | a.l:=m *) 5102 ` obj1 = OVAR1 of var 5103 | OBJ1 of (string # method1) list 5104 | INVOKE1 of obj1 => string 5105 | UPDATE1 of obj1 => string => method1 ; 5106 5107 (* method1 ::= sigma(x)a *) 5108 method1 = SIGMA1 of var => obj1 ` ; 5109\end{verbatim} 5110 5111\noindent 5112This creates the new mutually recursive types {\tt obj1} and {\tt method1}, 5113and also the constructor functions 5114 5115\begin{center} 5116\begin{tabular}[t]{l@{\hspace{0.5cm}}c@{\hspace{0.5cm}}l} 5117{\tt OVAR1} & {\tt :} & {\tt var -> obj1} \\ 5118{\tt OBJ1} & {\tt :} & {\tt (string \# method1) list -> obj1} \\ 5119{\tt INVOKE1} & {\tt :} & {\tt obj1 -> string -> obj1} \\ 5120{\tt UPDATE1} & {\tt :} & {\tt obj1 -> string -> method1 -> obj1} \\ 5121{\tt SIGMA1} & {\tt :} & {\tt var -> obj1 -> method1} \\ 5122\end{tabular} 5123\end{center} 5124 5125It also creates associated theorems for induction, function existance, 5126and one-to-one and distinctiveness properties of the constructors. 5127 5128The definition above goes beyond 5129%is more sophisticated than 5130simple mutual recursion 5131of types, to involve what is called ``nested recursion,'' where a type 5132being defined may appear deeply nested under type operators such as 5133{\tt list}, {\tt prod}, or {\tt sum}. In the above definition, 5134in the line defining 5135the {\tt OBJ1} constructor function, the type {\tt method1} is nested, 5136first as the right part of a pair type, and then as the element type of 5137a list type. 5138 5139The {\tt Hol\_definition} tool automatically compensates for this 5140complexity, creating in effect {\bf \it four\/} new types, not simply two. 5141It is as if the tool created the intermediate types 5142 5143\begin{center} 5144\begin{tabular}[t]{l@{\hspace{0.5cm}}c@{\hspace{0.5cm}}l} 5145{\tt entry1} & {\tt =} & {\tt string \# method1} \\ 5146{\tt dict1} & {\tt =} & {\tt (entry1)list} 5147\end{tabular} 5148\end{center} 5149 5150\noindent 5151except that these types are actually formed by the 5152{\tt prod} 5153and 5154{\tt list} 5155type operators, not by creating new types. 5156%Then the {\tt OBJ1} constructor could have been defined 5157%as {\tt OBJ1 of dict1}. 5158It turns out that when defining mutually recursive functions on these 5159types, there must be {\it four} related functions defined simultaneously, 5160one for each of the types 5161{\tt obj1}, {\tt dict1}, {\tt entry1}, and {\tt method1}. 5162Similarly, when proving theorems about these functions, 5163one must use mutually recursive structural induction, 5164where the goal has four parts, one for each of the types. 5165 5166% 5167%In fact, it is handled somewhat as if the user had typed, 5168% 5169%\begin{verbatim} 5170%val _ = Hol_datatype 5171% 5172% (* obj1 ::= x | d | a.l | a.l:=m *) 5173% ` obj1 = OVAR1 of var 5174% | OBJ1 of dict1 5175% | INVOKE1 of obj1 => string 5176% | UPDATE1 of obj1 => string => method1 ; 5177% 5178% (* dict1 ::= [] | e :: d *) 5179% dict1 = NIL 5180% | CONS of entry1 => dict1 ; 5181% 5182% (* entry ::= s = m *) 5183% entry1 = MK_PAIR of string => method1 ; 5184% 5185% (* method1 ::= sigma(x)a *) 5186% method1 = SIGMA1 of var => obj1 ` ; 5187%\end{verbatim} 5188% 5189%\noindent 5190%except that the constructor functions {\tt NIL}, {\tt CONS}, and 5191%{\tt MK\_PAIR} already exist. Using the nested recursion form, as 5192%first given, 5193%means that the types corresponding to {\tt dict1} and 5194%{\tt entry1} in the second form are actually represented as nested 5195%combinations of {\tt obj1} and {\tt method1}. 5196% 5197%\begin{center} 5198%\begin{tabular}[t]{l@{\hspace{0.5cm}}l} 5199%{\tt dict1} & {\tt = (string \# method1)list} \\ 5200%{\tt entry1} & {\tt = string \# method1} 5201%\end{tabular} 5202%\end{center} 5203% 5204%For clarity's sake, we will henceforth use the names {\tt dict1} and 5205%{\tt entry1} as abbreviations for the longer true types given above. 5206% 5207%The nested version is advantageous over the larger, 5208%non-nested version, 5209%because it means that these types are in fact real lists and pairs, 5210%and we can use all of the well-developed support in HOL to deal with 5211%lists and pairs, without having to reinvent the wheel and redo all 5212%that work for {\tt dict1} and {\tt entry1}. 5213 5214%The constructors for {\tt obj1} and {\tt method1} 5215%have the following types. 5216% 5217%\begin{center} 5218%\begin{tabular}[t]{l@{\hspace{0.5cm}}l} 5219%{\tt OVAR1} & {\tt : var -> obj1} \\ 5220%{\tt OBJ1} & {\tt : dict1 -> obj1} \\ 5221%{\tt INVOKE1} & {\tt : obj1 -> string -> obj1} \\ 5222%{\tt UPDATE1} & {\tt : obj1 -> string -> method1 -> obj1} \\ 5223%{\tt SIGMA1} & {\tt : var -> obj1 -> method1} 5224%\end{tabular} 5225%\end{center} 5226% 5227%Note that the constructor functions {\tt NIL}, {\tt CONS}, and 5228%{\tt MK\_PAIR} already apply correctly without modification, 5229%because they are polymorphic. 5230% 5231%\begin{center} 5232%\begin{tabular}[t]{l@{\hspace{0.5cm}}l} 5233%{\tt NIL} & {\tt : dict1} \\ 5234%{\tt CONS} & {\tt : entry1 -> dict1 -> dict1} \\ 5235%{\tt MK\_PAIR} & {\tt : string -> method1 -> entry1} 5236%\end{tabular} 5237%\end{center} 5238 5239%This mutually recursive type structure has ramifications wherever these 5240%new types are used. 5241%In particular, it affects how new mutually recursive functions on 5242%values of these types are defined, and it affects how theorems about 5243%the properties of those mutually recursive functions are proven by 5244%mutually recursive structural induction. 5245 5246%As mentioned before, there are several theorems proven 5247%automatically and stored in the current theory. 5248%These concern such things as an induction principle and 5249%the distinctiveness and one-to-one properties of constructors. 5250 5251Now we will construct the pure sigma calculus from the pre-sigma calculus. 5252%Now, to construct the pure sigma calculus from the pre-sigma calculus, 5253%we will need to form quotients of these four types by their alpha-equivalence 5254%relations. 5255 5256 5257% 5258\section{The Pure Sigma Calculus in HOL} 5259% 5260\label{puresigmacalculus} 5261 5262We here define the pure sigma calculus in HOL. 5263 5264Let us assume 5265that we have defined alpha-equivalence relations for each of the two types 5266{\tt obj1} 5267%{\tt dict1}, {\tt entry1}, 5268and {\tt method1}, called 5269{\tt ALPHA\_obj} 5270%{\tt ALPHA\_dict}, {\tt ALPHA\_entry}, 5271and {\tt ALPHA\_method}, 5272and that we have proven the 5273%reflexivity, symmetry, and transitivity of each of these, as theorems called 5274equivalence theorems for these, 5275%{\tt ALPHA\_obj\_REFL}, 5276%{\tt ALPHA\_obj\_SYM}, 5277%{\tt ALPHA\_obj\_TRANS}, et cetera. 5278\begin{center} 5279\begin{tabular}{l} 5280{\tt ALPHA\_obj\_EQUIV:} \\ 5281\hspace{0.9cm} 5282{\tt $\vdash \forall$x y. ALPHA\_obj x y = (ALPHA\_obj x = ALPHA\_obj y)} \\ 5283{\tt ALPHA\_method\_EQUIV:} \\ 5284\hspace{0.9cm} 5285{\tt $\vdash \forall$x y. ALPHA\_method x y =\;(ALPHA\_method x = ALPHA\_method y)} 5286\end{tabular} 5287\end{center} 5288 5289We specify the constants that are to be lifted: 5290\begin{verbatim} 5291- val defs = [{def_name="OVAR_def", fname="OVAR", 5292 func= (--`OVAR1`--), fixity=NONE}, 5293 {def_name="OBJ_def", fname="OBJ", 5294 func= (--`OBJ1`--), fixity=NONE}, 5295 {def_name="INVOKE_def", fname="INVOKE", 5296 func= (--`INVOKE1`--), fixity=NONE}, 5297 {def_name="UPDATE_def", fname="UPDATE", 5298 func= (--`UPDATE1`--), fixity=NONE}, 5299 {def_name="SIGMA_def", fname="SIGMA", 5300 func= (--`SIGMA1`--), fixity=NONE}, 5301 {def_name="HEIGHT_def", fname="HEIGHT", 5302 func= (--`HEIGHT1`--), fixity=NONE}, 5303 {def_name="FV_def", fname="FV", 5304 func= (--`FV1`--), fixity=NONE}, 5305 {def_name="SUB_def", fname="SUB", 5306 func= (--`SUB1`--), fixity=NONE}, 5307 {def_name="FV_subst_def", fname="FV_subst", 5308 func= (--`FV_subst1`--), fixity=NONE}, 5309 {def_name="SUBo_def", fname="SUBo", 5310 func= (--`SUB1o :^obj -> ^subs -> ^obj`--), 5311 fixity=SOME(Infix(NONASSOC,150))}, 5312 {def_name="SUBd_def", fname="SUBd", 5313 func= (--`SUB1d :^dict -> ^subs -> ^dict`--), 5314 fixity=SOME(Infix(NONASSOC,150))}, 5315 {def_name="SUBe_def", fname="SUBe", 5316 func= (--`SUB1e :^entry -> ^subs -> ^entry`--), 5317 fixity=SOME(Infix(NONASSOC,150))}, 5318 {def_name="SUBm_def", fname="SUBm", 5319 func= (--`SUB1m :^method -> ^subs -> ^method`--), 5320 fixity=SOME(Infix(NONASSOC,150))}, 5321 {def_name="vsubst_def", fname="/", 5322 func= (--`$//`--), fixity=SOME(Infix(NONASSOC,150))}, 5323 ... 5324 ]; 5325\end{verbatim} 5326 5327We specify the respectfulness theorems to assist the lifting: 5328\begin{verbatim} 5329 5330val respects = 5331 [OVAR1_RSP, OBJ1_RSP, INVOKE1_RSP, UPDATE1_RSP, SIGMA1_RSP, 5332 HEIGHT_obj1_RSP, HEIGHT_dict1_RSP, HEIGHT_entry1_RSP, 5333 HEIGHT_method1_RSP, FV_obj1_RSP, FV_dict1_RSP, FV_entry1_RSP, 5334 FV_method1_RSP, SUB1_RSP, FV_subst_RSP, vsubst1_RSP, 5335 SUBo_RSP, SUBd_RSP, SUBe_RSP, SUBm_RSP, 5336 ... ] 5337\end{verbatim} 5338 5339We specify the polymorphic 5340preservation 5341%``definitions'' 5342theorems to assist the lifting: 5343\begin{verbatim} 5344val polyprs = [BV_subst_PRS, COND_PRS, CONS_PRS, NIL_PRS, 5345 COMMA_PRS, FST_PRS, SND_PRS, 5346 LET_PRS, o_PRS, UNCURRY_PRS, 5347 FORALL_PRS, EXISTS_PRS, 5348 EXISTS_UNIQUE_PRS, ABSTRACT_PRS]; 5349\end{verbatim} 5350 5351We specify the polymorphic respectfulness theorems 5352to assist the lifting: 5353\begin{verbatim} 5354val polyrsp = [BV_subst_RSP, COND_RSP, CONS_RSP, NIL_RSP, 5355 COMMA_RSP, FST_RSP, SND_RSP, 5356 LET_RSP, o_RSP, UNCURRY_RSP, 5357 RES_FORALL_RSP, RES_EXISTS_RSP, 5358 RES_EXISTS_EQUIV_RSP, RES_ABSTRACT_RSP]; 5359\end{verbatim} 5360 5361The old theorems to be lifted are too many to list, but some will 5362be shown later. 5363\begin{verbatim} 5364- val old_thms = [...]; 5365\end{verbatim} 5366 5367We now define the pure sigma calculus types {\tt obj} and {\tt method}, 5368and lift all constants and theorems: 5369 5370\begin{verbatim} 5371- val new_thms = 5372 define_quotient_types 5373 {types = [{name = "obj", equiv = ALPHA_obj_EQUIV}, 5374 {name = "method", equiv = ALPHA_method_EQUIV}], 5375 defs = defs, 5376 tyop_equivs = [LIST_EQUIV, PAIR_EQUIV], 5377 tyop_quotients = [LIST_QUOTIENT, PAIR_QUOTIENT, 5378 FUN_QUOTIENT], 5379 tyop_simps = [LIST_REL_EQ, LIST_MAP_I, 5380 PAIR_REL_EQ, PAIR_MAP_I, 5381 FUN_REL_EQ, FUN_MAP_I], 5382 respects = respects, 5383 poly_preserves = polyprs, 5384 poly_respects = polyrsp, 5385 old_thms = old_thms}; 5386\end{verbatim} 5387 5388The tool is able to lift many theorems to the abstract, quotient level. 5389Here is the original definition of substitution on a variable: 5390{\tt \begin{tabbing} 5391$\vdash$ \=($\forall$y. SUB1 [] y = OVAR1 y) $\wedge$ \\ 5392\> ($\forall$y x c s. SUB1 ((x,c)::s) y = (if y = x then c else SUB1 s y)) 5393\end{tabbing}} 5394This theorem lifts to its abstract version: 5395{\tt \begin{tabbing} 5396$\vdash$ \=($\forall$y. SUB [] y = OVAR y) $\wedge$ \\ 5397\> ($\forall$y x c s. SUB ((x,c)::s) y = (if y = x then c else SUB s y)) 5398\end{tabbing}} 5399Note how the different constants lift, e.g., {\tt SUB1} to {\tt SUB}, 5400{\tt OVAR1} to {\tt OVAR}. Also note that the quantification of 5401{\tt c:obj1} has now become of {\tt obj}. 5402What may not be so obvious is how the 5403polymorphic operators lift to the abstract versions of themselves: 5404{\tt []}, {\tt ,}, {\tt ::}, {\tt if...then...else}. 5405In fact, though the operators look the same, all the types have changed 5406from the lower to the higher versions. 5407Proving this lifted theorem took considerable automation, 5408hidden behind 5409%which may not be apparent from 5410the simplicity of the result. 5411In addition, the original theorem was not regular; before lifting, 5412it actually was first quietly converted to: 5413{\tt \begin{tabbing} 5414$\vdash$ \=($\forall$y. ALPHA\_obj (SUB1 [] y) (OVAR1 y)) $\wedge$ \\ 5415\> (\=$\forall$y x \=(c :: respects ALPHA\_obj) \\ 5416\>\>\> (s :: respects (LIST\_REL (\$= \#\#\# ALPHA\_obj))). \\ 5417\>\> ALPHA\_obj (SUB1 ((x,c)::s) y) (if y = x then c else SUB1 s y)) 5418\end{tabbing}} 5419 5420Similarly, here is a version of this definition which uses the {\tt let...in} 5421form: 5422{\tt \begin{tabbing} 5423$\vdash$ \=($\forall$p\=\ s y. \\ 5424\>\> SUB1 (p::s) y = \\ 5425\>\> (let (x,c) = p in (if y = x then c else SUB1 s y))) $\wedge$ \\ 5426\> ($\forall$y. SUB1 [] y = OVAR1 y) 5427\end{tabbing}} 5428This lifts to the following abstract version: 5429{\tt \begin{tabbing} 5430$\vdash$ \=($\forall$p\=\ s y. \\ 5431\>\> SUB (p::s) y = \\ 5432\>\> (let (x,c) = p in (if y = x then c else SUB s y))) $\wedge$ \\ 5433\> ($\forall$y. SUB [] y = OVAR y) 5434\end{tabbing}} 5435In addition to the previous issues, this involves the {\tt LET} 5436operator, which is higher-order, taking a function as an argument. 5437Furthermore, because the {\tt let} involves a pair, the 5438pair is implemented by the {\tt UNCURRY} operator, which is also higher-order. 5439The following regular version was quietly proven and then lifted: 5440{\tt \begin{tabbing} 5441$\vdash$ \=($\forall$(\=p\=\ :: respects (\$= \#\#\# ALPHA\_obj)) \\ 5442\>\>\> (s :: respects (LIST\_REL (\$= \#\#\# ALPHA\_obj))) y. \\ 5443\>\> AL\=PHA\_obj (SUB1 (p::s) y) \\ 5444\>\>\> (LE\=T \\ 5445\>\>\>\> (UN\=CURRY \\ 5446\>\>\>\>\> ($\lambda$x\=\ (c::respects ALPHA\_obj). \\ 5447\>\>\>\>\>\> (if y = x then c else SUB1 s y))) p)) $\wedge$ \\ 5448\> ($\forall$y. ALPHA\_obj (SUB1 [] y) (OVAR1 y)) 5449\end{tabbing}} 5450 5451One of the most difficult theorems to lift is the induction theorem, 5452because it is higher-order, as it involves quantification over predicates. 5453{\tt \begin{tabbing} 5454$\vdash \forall$P\=0 P1 P2 P3. \\ 5455\> ($\forall$v. P0 (OVAR1 v)) $\wedge$ ($\forall$l. P2 l $\Rightarrow$ P0 (OBJ1 l)) $\wedge$ \\ 5456\> ($\forall$o'. P0 o' $\Rightarrow$ $\forall$s. P0 (INVOKE1 o' s)) $\wedge$ \\ 5457\> ($\forall$o' m. P0 o' $\wedge$ P1 m $\Rightarrow$ $\forall$s. P0 (UPDATE1 o' s m)) $\wedge$ \\ 5458\> ($\forall$o'. P0 o' $\Rightarrow$ $\forall$v. P1 (SIGMA1 v o')) $\wedge$ P2 [] $\wedge$ \\ 5459\> ($\forall$p l. P3 p $\wedge$ P2 l $\Rightarrow$ P2 (p::l)) $\wedge$ \\ 5460\> ($\forall$m. P1 m $\Rightarrow$ $\forall$s. P3 (s,m)) $\Rightarrow$ \\ 5461\> ($\forall$o'. P0 o') $\wedge$ ($\forall$m. P1 m) $\wedge$ ($\forall$l. P2 l) $\wedge$ ($\forall$p. P3 p) 5462\end{tabbing}} 5463This lifts to the abstract version: 5464{\tt \begin{tabbing} 5465$\vdash \forall$P\=0 P1 P2 P3. \\ 5466\> ($\forall$v. P0 (OVAR v)) $\wedge$ ($\forall$l. P2 l $\Rightarrow$ P0 (OBJ l)) $\wedge$ \\ 5467\> ($\forall$o'. P0 o' $\Rightarrow$ $\forall$s. P0 (INVOKE o' s)) $\wedge$ \\ 5468\> ($\forall$o' m. P0 o' $\wedge$ P1 m $\Rightarrow$ $\forall$s. P0 (UPDATE o' s m)) $\wedge$ \\ 5469\> ($\forall$o'. P0 o' $\Rightarrow$ $\forall$v. P1 (SIGMA v o')) $\wedge$ P2 [] $\wedge$ \\ 5470\> ($\forall$p l. P3 p $\wedge$ P2 l $\Rightarrow$ P2 (p::l)) $\wedge$ \\ 5471\> ($\forall$m. P1 m $\Rightarrow$ $\forall$s. P3 (s,m)) $\Rightarrow$ \\ 5472\> ($\forall$o'. P0 o') $\wedge$ ($\forall$m. P1 m) $\wedge$ ($\forall$l. P2 l) $\wedge$ ($\forall$p. P3 p) 5473\end{tabbing}} 5474Note how the quantifications over {\tt P0:obj1 -> bool}, etc. lift to 5475quantification over {\tt P0:obj -> bool}, etc. 5476The following regular version was quietly proven and then lifted: 5477{\tt \begin{tabbing} 5478$\vdash \forall$(\=P0\=::respects (ALPHA\_obj ===> \$=)) \\ 5479\>\> (P1::respects (ALPHA\_method ===> \$=)) \\ 5480\>\> (P2::respects (LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=)) \\ 5481\>\> (P3::respects ((\$= \#\#\# ALPHA\_method) ===> \$=)). \\ 5482\> ($\forall$v. P0 (OVAR1 v)) $\wedge$ \\ 5483\> ($\forall$l\=::respects (LIST\_REL (\$= \#\#\# ALPHA\_method)). \\ 5484\>\> P2 l $\Rightarrow$ P0 (OBJ1 l)) $\wedge$ \\ 5485\> ($\forall$o'::respects ALPHA\_obj. P0 o' $\Rightarrow$ $\forall$s. P0 (INVOKE1 o' s)) $\wedge$ \\ 5486\> ($\forall$(o'::respects ALPHA\_obj) (m::respects ALPHA\_method). \\ 5487\>\> P0 o' $\wedge$ P1 m $\Rightarrow$ $\forall$s. P0 (UPDATE1 o' s m)) $\wedge$ \\ 5488\> ($\forall$o'::respects ALPHA\_obj. P0 o' $\Rightarrow$ $\forall$v. P1 (SIGMA1 v o')) $\wedge$ \\ 5489\> P2 [] $\wedge$ \\ 5490\> ($\forall$(\=p\=::respects (\$= \#\#\# ALPHA\_method)) \\ 5491\>\>\> (l::respects (LIST\_REL (\$= \#\#\# ALPHA\_method))). \\ 5492\>\> P3 p $\wedge$ P2 l $\Rightarrow$ P2 (p::l)) $\wedge$ \\ 5493\> ($\forall$m::respects ALPHA\_method. P1 m $\Rightarrow$ $\forall$s. P3 (s,m)) $\Rightarrow$ \\ 5494\> ($\forall$o'::respects ALPHA\_obj. P0 o') $\wedge$ \\ 5495\> ($\forall$m::respects ALPHA\_method. P1 m) $\wedge$ \\ 5496\> ($\forall$l::respects (LIST\_REL (\$= \#\#\# ALPHA\_method)). P2 l) $\wedge$ \\ 5497\> ($\forall$p::respects (\$= \#\#\# ALPHA\_method). P3 p) 5498\end{tabbing}} 5499 5500Finally, the most difficult theorem to lift is the function existance 5501theorem, after the style proposed by Gordon and Melham \cite{GoMe96}. 5502This uses higher-order unique existance quantification, 5503%with sensitive semantics. 5504where the unique existance is not of a simple function, 5505but a tuple of four functions, involving a higher-order 5506\quotient{} relation of tuples of functions. This relation is {\it not\/} 5507an equivalence relation. 5508{\tt \begin{tabbing} 5509$\vdash$ \=$\forall$var \\ 5510\> (obj::respects(\$= ===> LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=)) \\ 5511\> (inv::respects(\$= ===> ALPHA\_obj ===> \$= ===> \$=)) \\ 5512\> (\=upd::respects \\ 5513\>\>(\$= ===> \$= ===> ALPHA\_obj ===> \$= ===> ALPHA\_method ===> \$=)) \\ 5514\> (\=cns::respects(\$\= = ===> \$= ===> (\$= \#\#\# ALPHA\_method) ===> \\ 5515\>\>\> LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=)) \\ 5516\>\>nil (par::respects(\$= ===> \$= ===> ALPHA\_method ===> \$=)) \\ 5517\> (s\=gm::respects(\$= ===> (\$= ===> ALPHA\_obj) ===> \$=)). \\ 5518\>\> $\exists !$\=(hom\=\_o,hom\_d,hom\_e,hom\_m)::respects \\ 5519\>\>\>\> (\=(ALPHA\_obj ===> \$=) \#\#\# \\ 5520\>\>\>\>\> (LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=) \#\#\# \\ 5521\>\>\>\>\> ((\$= \#\#\# ALPHA\_method) ===> \$=) \#\#\# \\ 5522\>\>\>\>\> (ALPHA\_method ===> \$=)). \\ 5523\>\>\>($\forall$x. hom\_o (OVAR1 x) = var x) $\wedge$ \\ 5524\>\>\>($\forall$d. hom\_o (OBJ1 d) = obj (hom\_d d) d) $\wedge$ \\ 5525\>\>\>($\forall$a l. hom\_o (INVOKE1 a l) = inv (hom\_o a) a l) $\wedge$ \\ 5526\>\>\>($\forall$a l m. hom\=\_o (UPDATE1 a l m) = \\ 5527\>\>\>\> upd (hom\_o a) (hom\_m m) a l m) $\wedge$ \\ 5528\>\>\>($\forall$e d. hom\_d (e::d) = cns (hom\_e e) (hom\_d d) e d) $\wedge$ \\ 5529\>\>\>(hom\_d [] = nil) $\wedge$ \\ 5530\>\>\>($\forall$l m. hom\_e (l,m) = par (hom\_m m) l m) $\wedge$ \\ 5531\>\>\>($\forall$x a. hom\=\_m (SIGMA1 x a) = \\ 5532\>\>\>\> sgm \=($\lambda$y. hom\_o (a <[ [(x,OVAR1 y)])) \\ 5533\>\>\>\>\> ($\lambda$y. a <[ [(x,OVAR1 y)])) 5534\end{tabbing}} 5535% old: 5536%\begin{verbatim} 5537%|- !var obj inv upd cns nil par sgm. 5538% ?!(hom_o,hom_d,hom_e,hom_m)::respects 5539% ((ALPHA_obj ===> $=) ### 5540% (LIST_REL ($= ### ALPHA_method) ===> $=) ### 5541% (($= ### ALPHA_method) ===> $=) ### 5542% (ALPHA_method ===> $=)). 5543% (!x. hom_o (OVAR1 x) = var x) /\ 5544% (!d. hom_o (OBJ1 d) = obj (hom_d d)) /\ 5545% (!a l. hom_o (INVOKE1 a l) = inv (hom_o a) l) /\ 5546% (!a l m. hom_o (UPDATE1 a l m) = 5547% upd (hom_o a) l (hom_m m)) /\ 5548% (!e d. hom_d (e::d) = cns (hom_e e) (hom_d d)) /\ 5549% (hom_d [] = nil) /\ 5550% (!l m. hom_e (l,m) = par l (hom_m m)) /\ 5551% !x a. hom_m (SIGMA1 x a) = 5552% sgm (\y. hom_o (a <[ [(x,OVAR1 y)])) 5553%\end{verbatim} 5554This lifts to the abstract version: 5555{\tt \begin{tabbing} 5556$\vdash \forall$v\=ar obj inv upd cns nil par sgm. \\ 5557\> $\exists !$\=(hom\_o,hom\_d,hom\_e,hom\_m). \\ 5558\>\> ($\forall$x. hom\_o (OVAR x) = var x) $\wedge$ \\ 5559\>\> ($\forall$d. hom\_o (OBJ d) = obj (hom\_d d) d) $\wedge$ \\ 5560\>\> ($\forall$a l. hom\_o (INVOKE a l) = inv (hom\_o a) a l) $\wedge$ \\ 5561\>\> ($\forall$a l m. hom\=\_o (UPDATE a l m) = \\ 5562\>\>\> upd (hom\_o a) (hom\_m m) a l m) $\wedge$ \\ 5563\>\> ($\forall$e d. hom\_d (e::d) = cns (hom\_e e) (hom\_d d) e d) $\wedge$ \\ 5564\>\> (hom\_d [] = nil) $\wedge$ \\ 5565\>\> ($\forall$l m. hom\_e (l,m) = par (hom\_m m) l m) $\wedge$ \\ 5566\>\> ($\forall$x a. hom\=\_m (SIGMA x a) = \\ 5567\>\>\> sgm \=($\lambda$y. hom\_o (a SUBo [(x,OVAR y)])) \\ 5568\>\>\>\> ($\lambda$y. a SUBo [(x,OVAR y)])) 5569\end{tabbing}} 5570% 5571% old: 5572%\begin{verbatim} 5573%|- !var obj inv upd cns nil par sgm. 5574% ?!(hom_o,hom_d,hom_e,hom_m). 5575% (!x. hom_o (OVAR x) = var x) /\ 5576% (!d. hom_o (OBJ d) = obj (hom_d d)) /\ 5577% (!a l. hom_o (INVOKE a l) = inv (hom_o a) l) /\ 5578% (!a l m. hom_o (UPDATE a l m) = 5579% upd (hom_o a) l (hom_m m)) /\ 5580% (!e d. hom_d (e::d) = cns (hom_e e) (hom_d d)) /\ 5581% (hom_d [] = nil) /\ 5582% (!l m. hom_e (l,m) = par l (hom_m m)) /\ 5583% !x a. hom_m (SIGMA x a) = 5584% sgm (\y. hom_o (a SUBo [(x,OVAR y)])) 5585%\end{verbatim} 5586 5587\noindent 5588Note how the restricted unique existance quantification 5589over {\tt (hom\_o :obj1->'a, 5590...)} 5591%..., hom\_m :method1 -> 'd)} 5592lifts to unique existance quantification over {\tt (hom\_o :obj->'a, 5593...)}. 5594%..., hom\_m :method -> 'd)}. 5595To accomplish this, 5596the following regular version was quietly proven and then lifted: 5597{\tt \begin{tabbing} 5598$\vdash$ \=$\forall$var \\ 5599\> (obj::respects(\$= ===> LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=)) \\ 5600\> (inv::respects(\$= ===> ALPHA\_obj ===> \$=)) \\ 5601\> (\=upd::respects \\ 5602\>\>(\$= ===> \$= ===> ALPHA\_obj ===> \$= ===> ALPHA\_method ===> \$=)) \\ 5603\> (\=cns::respects(\=\$= ===> \$= ===> (\$= \#\#\# ALPHA\_method) ===> \\ 5604\>\>\> LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=)) \\ 5605\>\>nil \\ 5606\> (par::respects (\$= ===> \$= ===> ALPHA\_method ===> \$=)) \\ 5607\> (sgm\=::respects (\$= ===> (\$= ===> ALPHA\_obj) ===> \$=)). \\ 5608\>\> $\exists !!$\=(hom\=\_o,hom\_d,hom\_e,hom\_m):: \\ 5609\>\>\>\> (ALPHA\_obj ===> \$=) \#\#\# \\ 5610\>\>\>\> (LIST\_REL (\$= \#\#\# ALPHA\_method) ===> \$=) \#\#\# \\ 5611\>\>\>\> ((\$= \#\#\# ALPHA\_method) ===> \$=) \#\#\# \\ 5612\>\>\>\> (ALPHA\_method ===> \$=). \\ 5613\>\>\>($\forall$x. hom\_o (OVAR1 x) = var x) $\wedge$ \\ 5614\>\>\>($\forall$d::\=respects (LIST\_REL (\$= \#\#\# ALPHA\_method)). \\ 5615\>\>\>\> hom\_o (OBJ1 d) = obj (hom\_d d) d) $\wedge$ \\ 5616\>\>\>($\forall$(a::respects ALPHA\_obj) l. \\ 5617\>\>\>\> hom\_o (INVOKE1 a l) = inv (hom\_o a) a l) $\wedge$ \\ 5618\>\>\>($\forall$(a::respects ALPHA\_obj) l (m::respects ALPHA\_method). \\ 5619\>\>\>\> hom\=\_o (UPDATE1 a l m) = \\ 5620\>\>\>\>\> upd (hom\_o a) (hom\_m m) a l m) $\wedge$ \\ 5621\>\>\>($\forall$\=(e::respects (\$= \#\#\# ALPHA\_method)) \\ 5622\>\>\>\>(d:\=:respects (LIST\_REL (\$= \#\#\# ALPHA\_method))). \\ 5623\>\>\>\>\> hom\_d (e::d) = cns (hom\_e e) (hom\_d d) e d) $\wedge$ \\ 5624\>\>\>(hom\_d [] = nil) $\wedge$ \\ 5625\>\>\>($\forall$l (\=m::respects ALPHA\_method). \\ 5626\>\>\>\> hom\_e (l,m) = par (hom\_m m) l m) $\wedge$ \\ 5627\>\>\>($\forall$x (a::respects ALPHA\_obj). \\ 5628\>\>\>\> hom\=\_m (SIGMA1 x a) = \\ 5629\>\>\>\>\> sgm \=($\lambda$y. hom\_o (a <[ [(x,OVAR1 y)])) \\ 5630\>\>\>\>\>\> ($\lambda$y. a <[ [(x,OVAR1 y)])) 5631\end{tabbing}} 5632% old: 5633%\begin{verbatim} 5634%|- !var obj inv upd cns nil par sgm. 5635% RES_EXISTS_EQUIV 5636% ((ALPHA_obj ===> $=) ### 5637% (LIST_REL ($= ### ALPHA_method) ===> $=) ### 5638% (($= ### ALPHA_method) ===> $=) ### 5639% (ALPHA_method ===> $=)) 5640% (\(hom_o,hom_d,hom_e,hom_m). 5641% (!x. hom_o (OVAR1 x) = var x) /\ 5642% (!d::respects (LIST_REL ($= ### ALPHA_method)). 5643% hom_o (OBJ1 d) = obj (hom_d d)) /\ 5644% (!(a::respects ALPHA_obj) l. 5645% hom_o (INVOKE1 a l) = inv (hom_o a) l) /\ 5646% (!(a::respects ALPHA_obj) l (m::respects ALPHA_method). 5647% hom_o (UPDATE1 a l m) = upd (hom_o a) l (hom_m m)) /\ 5648% (!(e::respects ($= ### ALPHA_method)) 5649% (d::respects (LIST_REL ($= ### ALPHA_method))). 5650% hom_d (e::d) = cns (hom_e e) (hom_d d)) /\ 5651% (hom_d [] = nil) /\ 5652% (!l (m::respects ALPHA_method). 5653% hom_e (l,m) = par l (hom_m m)) /\ 5654% !x (a::respects ALPHA_obj). 5655% hom_m (SIGMA1 x a) = 5656% sgm (\y. hom_o (a <[ [(x,OVAR1 y)]))) 5657%\end{verbatim} 5658This automatic higher order lifting was not available before this package. 5659 5660Now we have 5661$\mbox{\tt SIGMA}\ x\ (\mbox{\tt OVAR}\ x) = 5662 \mbox{\tt SIGMA}\ y\ (\mbox{\tt OVAR}\ y)$, etc., as true equality 5663within the HOL logic, as intended. 5664This accomplishes the creation of the pure sigma calculus 5665by identifying alpha-equivalent terms. 5666 5667 5668% 5669\section{Conclusions} 5670% 5671\label{conclusions} 5672 5673We have implemented a package for mechanically defining higher-order 5674quotient types 5675which is a conservative, definitional extension of the HOL logic. 5676The package automatically lifts not only types, 5677but also constants and theorems from 5678the original level to the quotient level. 5679 5680\begin{comment} 5681\end{comment} 5682Higher order quotients require 5683%involves 5684%is accomplished through 5685the use of \quotient{} relations, 5686as symmetric and transitive but not necessarily reflexive on all 5687%elements of 5688their domains. 5689%This is necessary to treat 5690%higher order quotients, 5691%where elements should not be compared by reflexive relations. 5692\begin{comment} 5693\end{comment} 5694 5695The relationship between the lower type and the 5696%lifted, 5697quotient type 5698is characterized by the \quotient{} relation, the abstraction function, 5699and the representation function. 5700As a key contribution, 5701three necessary properties have been identified 5702for these to properly describe a quotient, 5703which are preserved in the creation of both 5704aggregate and higher order quotients. 5705Most normal polymorphic operators both respect and are preserved 5706across such quotients, including higher order quotients. 5707 5708The Axiom of Choice was used in this design. We showed that an alternative 5709design may be constructed without dependence on the Axiom of Choice, but that 5710it may not be extended to higher order quotients while remaining constructive. 5711 5712%Most implementations of quotients in theorem provers 5713%provided support for 5714%%the modeling of 5715%modeling 5716%the quotient types, 5717%given an equivalence relation. 5718Prior to this work, only Harrison 5719\cite{Har98} went beyond 5720%this 5721support for modeling the quotient types 5722to provide automation for the lifting of constant definitions 5723and theorems from their original statements concerning 5724the original types to the corresponding analogous statements 5725concerning the new quotient types. This is important 5726for the practical application of quotients to sizable problems like 5727quotients on 5728the syntax of 5729%large, 5730complex, 5731realistic programming or specification 5732%or annotation 5733%\linebreak 5734languages. 5735%The size of these grammars means that the number 5736%of theorems and their bulk are large, and there can be a 5737%significant amount of labor involved in lifting these definitions and 5738%theorems by hand. 5739These may be modelled 5740as recursive types, where 5741terms which are 5742partially equivalent by being 5743well-typed and alpha-equivalent 5744are identified by taking quotients. 5745This eases the traditional problem of the capture of bound variables 5746\cite{GoMe96}. 5747 5748Such quotients may now be more easily modeled within a theorem prover, 5749using the package described here. 5750 5751{\it Soli Deo Gloria.} 5752 5753 5754%\begin{appendix} 5755% 5756%% 5757%\section{Properties of Quotient Types} 5758%% 5759% 5760%Given a quotient theorem, 5761%%which is the defining property for the constants 5762%%{\it abs} and {\it rep}, 5763%there are several tools provided in the package 5764%that prove and return useful derivative results. 5765% 5766%\begin{center} 5767%\framebox{ 5768%\begin{tabular}[t]{l@{\hspace{0.5cm}}l} 5769%{\tt prove\_quotient\_rep\_abs\_equiv} & {\tt : thm -> thm} \\ 5770%{\tt prove\_quotient\_rep\_abs\_equal} & {\tt : thm -> thm} \\ 5771%{\tt prove\_quotient\_rep\_abs\_equal2} & {\tt : thm -> thm} \\ 5772%{\tt prove\_quotient\_equal\_is\_rep\_equiv} & {\tt : thm -> thm} \\ 5773%{\tt prove\_quotient\_rep\_fn\_one\_one} & {\tt : thm -> thm} \\ 5774%{\tt prove\_quotient\_abs\_iso\_equiv} & {\tt : thm -> thm} \\ 5775%{\tt prove\_quotient\_rep\_fn\_onto} & {\tt : thm -> thm} \\ 5776%{\tt prove\_quotient\_abs\_fn\_onto} & {\tt : thm -> thm} \\ 5777%{\tt prove\_quotient\_equiv} & {\tt : thm -> thm} \\ 5778%{\tt prove\_quotient\_equiv\_refl} & {\tt : thm -> thm} \\ 5779%{\tt prove\_quotient\_equiv\_sym} & {\tt : thm -> thm} \\ 5780%{\tt prove\_quotient\_equiv\_trans} & {\tt : thm -> thm} \\ 5781%\end{tabular} 5782%} 5783%\end{center} 5784% 5785%Each of these takes as its argument a quotient theorem of the form returned by 5786%{\tt define\_quotient\_type}: 5787% 5788%\begin{center} 5789%\tt 5790%|- (!a. {\it abs}({\it rep} a) = a) $\wedge$ 5791% (!r r'. {\it E\/} r r' = ({\it abs} r = {\it abs\/} r')) 5792%\end{center} 5793% 5794%If {\it th\/} is of this form, then evaluating 5795%{\tt prove\_quotient\_rep\_abs\_equiv} {\it th} proves that 5796%{\it rep} is the left inverse of {\it abs}, up to equivalence, 5797%%the representative of an equivalence class of a value 5798%%%the abstraction of the representative of a value 5799%%is equivalent to that value, 5800%returning the theorem: 5801% 5802%\begin{verse} \tt 5803% |- !r. {\it E\/} ({\it rep} ({\it abs} r)) r 5804%\end{verse} 5805% 5806%%Likewise, 5807%Evaluating 5808%{\tt prove\_quotient\_rep\_abs\_equal} {\it th} proves that 5809%%the representative of the abstraction 5810%the composition of {\it rep} with {\it abs} 5811%of a value has the same 5812%equivalence class as the original value: 5813% 5814%\begin{verse} \tt 5815% |- !r. {\it E\/} ({\it rep} ({\it abs} r)) = {\it E\/} r 5816%\end{verse} 5817% 5818%Evaluating 5819%{\tt prove\_quotient\_rep\_abs\_equal2} {\it th} proves 5820%a symmetric version of the same idea, both of which are useful 5821%for rewriting: 5822% 5823%\begin{verse} \tt 5824% |- !r r'. {\it E\/} r ({\it rep} ({\it abs} r')) = {\it E\/} r r' 5825%\end{verse} 5826% 5827%Evaluating 5828%{\tt prove\_quotient\_equal\_is\_rep\_equiv} {\it th} proves that 5829%equality between abstract values is equivalence between representatives: 5830% 5831%\begin{verse} \tt 5832% |- !a a'. (a = a') = {\it E\/} ({\it rep} a) ({\it rep} a') 5833%\end{verse} 5834% 5835%Evaluating 5836%{\tt prove\_quotient\_rep\_fn\_one\_one} {\it th} proves that 5837%{\it rep} is one-to-one: 5838% 5839%\begin{verse} \tt 5840% |- !a a'. ({\it rep} a = {\it rep} a') 5841% = (a = a') 5842%\end{verse} 5843% 5844%%Evaluating 5845%%{\tt prove\_quotient\_equiv\_rep\_one\_one} {\it th} proves that 5846%%the composition of {\it E\/} with {\it rep} is one-to-one: 5847%% 5848%%\begin{verse} \tt 5849%% |- !a a'. ({\it E\/} ({\it rep} a) = {\it E\/} ({\it rep} a')) 5850%% = (a = a') 5851%%\end{verse} 5852% 5853%Evaluating 5854%{\tt prove\_quotient\_abs\_iso\_equiv} {\it th} proves that 5855%{\it abs} and {\it E\/} 5856%are isomorphic with respect to equality: 5857% 5858%\begin{verse} \tt 5859% |- !r r'. ({\it abs} r = {\it abs} r') 5860% = ({\it E\/} r = {\it E\/} r') 5861%\end{verse} 5862% 5863%Evaluating 5864%{\tt prove\_quotient\_rep\_fn\_onto} {\it th} proves that 5865%{\it rep} is onto, up to equivalence: 5866% 5867%\begin{verse} \tt 5868% |- !r. ?a. {\it E\/} r ({\it rep} a) 5869%\end{verse} 5870% 5871%Evaluating 5872%{\tt prove\_quotient\_abs\_fn\_onto} {\it th} proves that 5873%{\it abs} is onto: 5874% 5875%\begin{verse} \tt 5876% |- !a. ?r. a = {\it abs} r 5877%\end{verse} 5878% 5879%Evaluating 5880%{\tt prove\_quotient\_equiv} {\it th} proves the equivalence theorem, 5881%that equivalence between elements is equality between equivalence classes: 5882% 5883%\begin{verse} \tt 5884% |- !x y. {\it E\/} x y = ({\it E\/} x = {\it E\/} y) 5885%\end{verse} 5886% 5887%Evaluating 5888%{\tt prove\_quotient\_equiv\_refl} {\it th} proves that 5889%{\it E\/} is reflexive: 5890% 5891%\begin{verse} \tt 5892% |- !x. {\it E\/} x x 5893%\end{verse} 5894% 5895%Evaluating 5896%{\tt prove\_quotient\_equiv\_sym} {\it th} proves that 5897%{\it E\/} is symmetric: 5898% 5899%\begin{verse} \tt 5900% |- !x y. {\it E\/} x y ==> {\it E\/} y x 5901%\end{verse} 5902% 5903%And evaluating 5904%{\tt prove\_quotient\_equiv\_trans} {\it th} proves 5905%that 5906%{\it E\/} is transitive: 5907% 5908%\begin{verse} \tt 5909% |- !x y z. {\it E\/} x y $\wedge$ 5910% {\it E\/} y z ==> {\it E\/} x z 5911%\end{verse} 5912% 5913%None of these functions saves anything in the current theory file. 5914%In fact, it should usually be unnecessary to save the results proved 5915%by these functions, since they can be generated quickly whenever required 5916%from the theorem returned by {\tt define\_quotient\_type}, which was 5917%itself saved. 5918% 5919%\end{appendix} 5920 5921 5922% 5923% ---- Bibliography ---- 5924% 5925\begin{thebibliography}{5} 5926% 5927\bibitem {AbCa96} 5928Abadi, M., Cardelli, L.: 5929{\it A Theory of Objects.} 5930Springer-Verlag 1996. 5931% 5932\bibitem {Bar81} 5933Barendregt,\:H.P.: 5934{\it The\,Lambda\,Calculus,\,Syntax\,and\,Semantics.} 5935North-Holland,\:1981. 5936% 5937\bibitem {BrM92} 5938Bruce, K., Mitchell, J.~C.: 5939`PER models of subtyping, recursive types and higher-order polymorphism', in 5940{\it Principles of Programming Languages 19}, 5941Albequerque, New Mexico, 1992, pp. 316-327. 5942% 5943\bibitem {CPS02} 5944Chicli, L., Pottier, L., Simpson C.: 5945`Mathematical Quotients and Quotient Types in Coq', 5946Proceedings of {\it TYPES 2002}, 5947%Berg en Dal, Netherlands, April 24-28, 2002, 5948Lecture Notes in Computer Science, vol. 2646 5949(Springer-Verlag, 2002). 5950% 5951\bibitem {End77} 5952Enderton, H.~B.: 5953{\it Elements of Set Theory.} 5954Academic Press, 1977. 5955% 5956\bibitem {GPWZ02} 5957Geuvers, H., Pollack, R., Wiekijk, F., Zwanenburg, J.: 5958`A constructive algebraic hierarchy in Coq', in 5959{\it Journal of Symbolic Computation}, 34(4), 2002, pp. 271-286. 5960% 5961\bibitem {GoMe93} 5962Gordon, M.~J.~C., Melham, T.~F.: 5963{\it Introduction to HOL.} 5964Cambridge University Press, Cambridge, 1993. 5965% 5966\bibitem {GoMe96} 5967Gordon, A.~D., Melham, T.~F.: 5968`Five Axioms of Alpha Conversion', in 5969{\it Theorem Proving in Higher Order Logics: 59709th International Conference, TPHOLs'96}, 5971edited by J. von Wright, J. Grundy and J. Harrison, 5972Lecture Notes in Computer Science, vol. 1125 5973(Springer-Verlag, 1996), pp. 173-190. 5974% 5975\bibitem {Har98} 5976Harrison, J.: 5977{\it Theorem Proving with the Real Numbers,} 5978\S{2.11}, pp. 33-37. 5979Springer-Verlag 1998. 5980% 5981\bibitem {Hof95} 5982Hofmann, M.: 5983`A simple model for quotient types,' in 5984{\it Typed Lambda Calculus and Applications}, 5985Lecture Notes in Computer Science, vol. 902 5986(Springer-Verlag, 1995), pp. 216-234. 5987% 5988%\bibitem {Hom01} 5989%Homeier, P.~V.: 5990%A Proof of the Church-Rosser Theorem 5991%for the Lambda Calculus 5992%in Higher Order Logic. 5993%Submitted to 5994%{\it 5995%14th International Conference on Theorem Proving in Higher Order Logics\/} 5996%(TPHOLs'01), 5997%Sept. 3-6, 2001, Edinburgh, Scotland. 5998% 5999%\bibitem {HoW01} 6000%Homeier, P.~V.: 6001%{\tt http://www.cis.upenn.edu/\verb+~+hol/lamcr}. 6002% 6003\bibitem {Kal89} 6004Kalker, T.: at 6005{\tt www.ftp.cl.cam.ac.uk/ftp/hvg/info-hol-archive/00xx/0082}. 6006% 6007\bibitem {Lei69} 6008Leisenring, A. C.: 6009{\it Mathematical Logic and Hilbert's $\varepsilon$-Symbol.} 6010Gordon and Breach, 1969. 6011% 6012\bibitem {Moore82} 6013Moore, G. H.: 6014{\it Zermelo's Axiom of Choice: It's Origins, Development, and Influence.} 6015Springer-Verlag 1982. 6016% 6017\bibitem {NiPaWe02} 6018Nipkow, T., Paulson, L.C., Wenzel, M.: 6019{\it Isabelle/HOL.} 6020Springer-Verlag 2002. 6021% 6022\bibitem {OwS01} 6023Owre, S., Shankar, N.: 6024{\it Theory Interpretations in PVS}, 6025Technical Report SRI-CSL-01-01, 6026Computer Science Laboratory, SRI International, 6027Menlo Park, CA, April 2001. 6028% 6029\bibitem {Nog02} 6030Nogin, A.: 6031`Quotient Types: A Modular Approach,' in 6032{\it Theorem Proving in Higher Order Logics: 603315th International Conference, TPHOLs 2002}, 6034edited by V.~A.~Carre\~{n}o, C.~Mu\~{n}oz, and S.~Tahar, 6035Lecture Notes in Computer Science, vol. 2410 6036(Springer-Verlag, 2002), pp. 263-280. 6037% 6038\bibitem {LP04} 6039Paulson, L.: 6040`Defining Functions on Equivalence Classes,' 6041{\it ACM Transactions on Computational Logic}, 6042in press. Previously issued as 6043Report, Computer Lab, University of Cambridge, April 20, 2004. 6044% 6045\bibitem {Rob89} 6046Robinson, E.: 6047`How Complete is PER?', 6048in {\it Fourth Annual Symposium on Logic in Computer Science\/} (LICS), 60491989, pp. 106-111. 6050% 6051\bibitem {Slo97} 6052Slotosch, O.: 6053`Higher Order Quotients and their Implementation in Isabelle HOL', in 6054{\it Theorem Proving in Higher Order Logics: 605510th International Conference, TPHOLs'97}, 6056edited by Elsa L. Gunter and Amy Felty, 6057Lecture Notes in Computer Science, vol. 1275 6058(Springer-Verlag, 1997), pp. 291-306. 6059% 6060\end{thebibliography} 6061 6062 6063 6064 6065% 6066\end{document} 6067