Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu, semaneth@cis.umassd.edu
In-Reply-To: <199405250252.AA11221@argo.cis.umassd.edu> (message from Sebastian Maneth on Wed, 25 May 1994 04:52:23 +0200)
Subject: Re: cut elimination in HOL
Message-Id: <94May25.123856met_dst.8111@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 25 May 1994 12:38:54 +0200


> I want to implement a form of cut elimination for higher order logic
> proofs, and I am wandering if HOL is the right system to use; or if I
> should rather make up my own data structures in e.g. ML. (it would be
> much nicer to use a package like HOL that has so many useful tools...)

> Has anyone done something like that in HOL, or knows a good way to do it?
> (with 'it' I mean applying rewrite rules to a proof, to implement cut
> elimination, or any proof manipulation)

HOL systems don't normally keep proofs. A HOL "proof" is an execution of
an ML function with range type "thm" and usually doesn't exist all at
once. For instance, consider applying the successor function to both
sides of an equality theorem:

    - Q.AP_TERM `SUC` (Q.num_CONV `1`); 

    val it = |- SUC 1 = SUC (SUC 0) : thm

The "Q.num_CONV `1`" creates a theorem that is available for garbage
collection after "Q.AP_TERM" is done with it: all that is left of the
"proof" is the evidence that it occurred, the theorem.

People often make the mistake of confusing tactics with proofs: a tactic
is merely one way that a person might build an ML function that will
produce a "thm".

Anyway, Wai Wong has implemented a system wherein real proofs are
tracked and held, in their entirety, in a single data structure. The
details can be found through xmosaic, in the Cambridge Tech Reports. Its
title is something like WW_306.ps.gz.

Konrad.