Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
Message-Id: <199308300905.AA20962@infix.cs.ruu.nl>
Subject: HOL improvement: to better document your proof
To: info-hol@dworshak.cs.uidaho.edu (hol mailing list)
Date: Mon, 30 Aug 1993 11:05:44 +0100 (METDST)
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 1878

  > John Harrison wrote:
  > 
  > > As promised at the Vancouver meeting, I'm organizing a survey to
  > > collect views on how the HOL system should be improved.
  > 
  > Here's my two cents, which I'm posting publicly since I'm interested
  > to know whether anyone already has a good idea:
  > 
  >     How to make HOL proofs more readable and closer to the ordinary
  >     "textbook style" presentation?
  > 
  > I think many of you have experiences of the following kind.
  > You developed a theory a couple of months ago.  For some reason
  > you need to look at it again and modify it.  But you find that
  > you can't read your own proofs!  The only way you can revive your
  > memory is to step through the proofs using the subgoal package.
  > So all the efforts you spent on coming up with these proofs are lost.

Hi Ching Tsun,

The LEMMA and DERIVATION package I presented in HOL meeting in
Vancouver is made because I had precisely the same problem as you
mentioned, namely documenting our HOL proofs.

You can read the report in the proceeding ("On the Style of Mechanical
Proving", by Wishnu Prasetya), but to shorten the story here is the
idea. Basically a considerably complicated HOL proof consists of
several 'creative' steps. Usualy each step can be proven from the
previos ones by some rewriting or resolutions whose details are
usually not interesting. What we are more interested in to record is
what the creative decisions are, and what are the intermediate
expressions/theorems look like after applying those decisions.

I use the LEMMA and DERIVATION package to document the creative steps
of my HOL proofs. Proofs written using this package also have the same
format as what you call 'text book' presentation format.

If there is interest I will be glad to share the code and documentation
of the package with anyone.

Best regard,

Wishnu Prasetya