
This page gives information about this proof of the ChurchRosser theorem. It contains postscript and PDF versions of the paper. It also contains the full source code for the Higher Order Logic theorem prover to perform all proofs described in the paper. In addition, this page describes packages of supporting software, which supply needed tools to support the automated proof in the Higher Order Logic theorem prover.
Quotient Types
(PDF).
Briefing charts in
postscript
and
PDF.
Given as a Category B paper at
TPHOLs'2001, the 14th International Conference on
Theorem Proving in Higher Order Logics,
Edinburgh, Scotland, September 36, 2001.
The source code for this proof also contains all the software packages mentioned below.
Here is a package for creating a new type as the quotient of an
existing type, divided into equivalence classes
according to an equivalence relation. The package
creates the new quotient type, defines functions to map back and
forth between the old and new types, and proves theorems about
their behavior.
It also supports defining a family of new types with the same
pair, sum, and list structure as the original types.
Paper:
postscript
and
pdf.
Code:
quotient.sig and
quotient.sml.
Myra Van Inwegen has written a package for defining
relations by mutually recursive rule induction.
This package automatically proves theorems for the new relations'
rules, the inversions of the rules, and weak and strong rule
induction principles.
The package has been ported to Hol98, version Taupo5 or Taupo6.
Code:
ind_rel.sig and
ind_rel.sml.
Myra's
original version was for Hol90.
Using Hol98 version Taupo5, one can create mutually
recursive types using the Hol_datatype
function.
In addition, one can define mutually recursive functions
according to the recursive structure of the types.
However, there is
no automation provided in the standard Taupo5 system
to prove theorems about these functions
by mutually recursive structural induction.
This capability is now provided here as a tactic,
MUTUAL_INDUCT_THEN
.
Code:
MutualIndThen.sig and
MutualIndThen.sml.
Here is a package to do rewriting of goals by the conclusions
of implications, even if the antecedents have not yet been proven.
The author calls this "conditional rewriting."
Code:
cond_rewrite.sig and
cond_rewrite.sml.
The author appreciates all comments. See the documentation for email address.