Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
To: info-hol@edu.uidaho.cs.ted
Subject: Re: referring to assumptions cont.
Date: Mon, 04 Nov 91 10:41:39 +0000
From: Paul.Curzon@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.710:04.10.91.10.42.01"@cl.cam.ac.uk>


Using ASSUME can also cause problems. I use ASSUME lots. I am working
on a large compiler proof incrementally. I initially proved
a simplified version of the compiler and am gradually adding features to
the language. Each time I perform a new iteration, new arguments are
added to my definitions, types change, etc. Unfortunately this means
that on each iteration I have to redo  the whole proof finding what the
assumptions have changed to and manually editing my proof script, even
when the underlying proof has not really changed. This takes a long
time and happens more often than major changes to HOL occur. Giving me
a mouse interface that included the full text would still mean I would
have to go through the whole proof by hand, though it would speed up
the process.

Tidying proofs by turning them into single tactics also makes the
process of rerunning proofs difficult. Using let helps (I had not
thought of doing that) but you still have to take it all apart again by
hand to see what is actually happening. It would be nice if there was a
tactic debuggger that let you single step through a complex tactic.

I could have tried to prove a complete compiler on my first
iteration but I am sure I would have got nowhere. This approach was
the best way to make the problem tractable for a mere mortal.

Also it is possible for HOL to change in a way  that causes
individual assumptions to change (eg become universally quantified
when they previously were not - I think I remember this happening in
the change to HOL12).

I am not a HOL wizard so am afraid I only have problems not solutions.


Paul Curzon.