Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: shepherd_david/uk_bristo_br@brx001.bristol.st.com
Date: Wed, 19 Jul 95 10:23:50 +0100
Message-Id: <H00000cf00524405@MHS>
In-Reply-To: <"9507190207.AA01330(a) mirtillo.usr.dsi.unimi.it *"@MHS>
Subject: easy HOL?
Mime-Version: 1.0
To: marco@mirtillo.usr.dsi.unimi.it
Cc: info-hol@cs.uidaho.edu
Content-Type: text/plain; charset=US-ASCII; name="Message text"
Content-Transfer-Encoding: 7bit

> I know it is a "bad" thing to rely on assumptions ordering.
> 
> The point I wanted to show with my posting was that a good
> way to improve ability of a novice user is to give him simple
> tactics to do simple works he feels "natural".

However it may be even more unhelpful to point novice users
towards methods that aren't reliable!

> This kind of tactics is good for a "startup" package, the
> novice HOLer may use to approach theorem proving. Obviously,
> because of their inelegance, inefficiency, non-portability,
> etc., they are strongly discouraged to normal users. But, 
> in the meantime, novices can (should) learn good way to do
> things.

Given that fairly direct manipulation of assumptions may be something
that a novice user may want to do (i.e. before they have mastered
the complexities of general theorem continuations), then perhaps
what is really needed is a simple introduction on how to "safely"
use assumptions -- e.g. examples of how to use ASSUME on an assumption
to feed into a tactic and perhaps a simple continuation like the
USE_THEN I sometimes used.

Another, more radical, suggestion that sometimes crops up is to
have some means of labelling assumptions as they go on the assumption
list so that they can be referred to by label rather than by number
which should more robust.

> This is my opinion: to give new users a quick and dirty way
> to get results. Their leaning curve will be slow, but they
> will be able to get results quickly. Perhaps this helps.

So long as when you get up the learning curve you don't have to
say "well, most of the methods you've learnt aren't really suitable
for large scale work so forget them all and start again".

DeS