### Higher Order Quotients package

Here is the Higher Order Quotient package for HOL.
This makes use of the dependent rewriting package described below.
Please note that these packages are now a standard part of the HOL4 system, versions Kananaskis-3 and above.
This is version 2.3 of this package, as of August 12, 2005.

quotient23.tar.gz.
(*Compressed tar archive, 61,171 bytes*)

### Relationship between the Axiom of Choice and Higher Order Quotients

This is a development of an alternative design for higher order quotients
which avoids use of the Axiom of Choice, as
presented in section 6 of the paper,
*A Design Structure for Higher Order Quotients*.

This is version 1.0 of this proof, as of February 17, 2005.

axiomofchoice.tar.gz.
(*Compressed tar archive, 15,807 bytes*)

__Examples__

The following examples of higher order quotients are presented in order from simplest to the most complex. They are present
in the HOL4 system, versions Kananaskis-4 and above, in the directory <HOL-root>/src/quotient/examples.

### Message Encryption and Decryption

This is a recreation using higher order quotients of an example of message encryption and decryption studied by Larry Paulson
in his paper, "Defining Functions on Equivalence Classes," to be published in ACM Transactions on Computational Logic, in
press as of August 2005, but available at Larry Paulson's website, at
http://www.cl.cam.ac.uk/users/lcp/papers/Reports/equivclasses.pdf.
This paper is exceptionally well written, and a pleasure to read.

msgScript.sml.
(*SML source code for HOL, 14,642 bytes*)

### Finite Sets

This creates finite sets as a new type in HOL4 as a quotient of lists, as described in the TPHOLs 2005 paper, "A Design Structure
for Higher Order Quotients," available in the TPHOLs 2005 conference proceedings published by Springer-Verlag, LNCS 3603.

finite_setScript.sml.
(*SML source code for HOL, 24,267 bytes*)

### Alternative Development of Finite Sets

This contains another approach to using higher order quotients to form finite sets as a new type as a quotient of lists, composed
by Michael Norrish. The equivalence relation is defined simply as extensionality. The reader is invited to compare this
development with the first approach above.

ext_finite_setScript.sml.
(*SML source code for HOL, 11,985 bytes*)

### Proof of the Church-Rosser Theorem for the Lambda Calculus

As an example exercising the quotients package, here is a proof of the Church-Rosser theorem for the lambda calculus. This
makes use of the higher order quotients package described above to lift the lambda calculus from a free algebra to a quotient
version which identifies alpha-equivalent terms.

This proof was described in a Track B paper at TPHOLs'01 in Edinburgh, UK,and published in Richard J. Boulton and Paul B.
Jackson, editors, *TPHOLs 2001: Supplemental Proceedings,* pages 207-222, Division of Informatics, University of Edinburgh,
September 2001, available as Informatics Research Report EDI-INF-RR-0046. This paper is available here as
postscript and
PDF. The paper refers to a outdated version of the quotient library, but shows its usefulness.

This is version 2.3 of this proof, as of April 27, 2007.

lambda23.tar.gz.
(*Compressed tar archive, 87,209 bytes*)

The source code for this proof includes some of the software packages mentioned at the bottom of this page.

### Proof of the Church-Rosser Theorem for the Sigma Calculus

As an example exercising the quotients package, here is a proof of the Church-Rosser theorem for the sigma calculus. This
is a nested mutually recursive object calculus, invented by Abadi and Cardelli in their book, "A Theory of Objects." This
example makes use of the higher order quotients package described above to lift the sigma calculus from a free algebra to
a quotient version which identifies alpha-equivalent terms.

There is no paper yet describing this proof. In that absence, the best guide to understanding it is the paper for the lambda
calculus proof above, as the two have the same structure and use the same ideas, except that the sigma calculus proof uses
mutual recursion in many forms.

This is version 2.1 of this proof, as of April 27, 2007.

sigma21.tar.gz.
(*Compressed tar archive, 91,966 bytes*)

The source code for this proof includes some of the software packages mentioned below.