This page gives information about this proof of the Church-Rosser 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.
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 3-6, 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
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
The package has been ported to Hol98, version Taupo-5 or Taupo-6.
Code: ind_rel.sig and ind_rel.sml.
Myra's original version was for Hol90.
Using Hol98 version Taupo-5, one can create mutually
recursive types using the
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 Taupo-5 system
to prove theorems about these functions
by mutually recursive structural induction.
This capability is now provided here as a tactic,
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.