Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <25540.9405260914@frogland.inmos.co.uk>
Subject: Re: Accessing Assumptions
To: black@leopard.cs.byu.edu (Paul "E." Black)
Date: Thu, 26 May 1994 10:14:05 +0100 (BST)
Cc: hol2000@leopard.cs.byu.edu
In-Reply-To: <9405251636.AA27350@puma.cs.byu.edu> from "Paul "E." Black" at May 25, 94 10:36:19 am
Content-Type: text
Content-Length: 1892

Paul "E." Black has said:
>      Kelly Hall <hall@leopard.cs.byu.edu> wrote
>           b) numbering assumptions and using their index in rewrite rules is
>              easier than FIRST_ASSUM and ASSUM_LIST, although it makes a proof
>              more 'brittle'.
> 
> I've thought about the assumption list, too.  One would like to refer
> to assumptions by the content, something like "... the assumption
> about m < x ..."  My suggestion is to refer to assumptions by a
> *signature* rather than a literal match (a textual copy) or an index.
> Hopefully the signature would change less often than either of those.

These suggestions have the effect of tying the user interface very
closely to the underlying logic system.

One way of handling this sort of thing is to develop the subgoal 
system into something that manipulates tactic trees. I.e. you use
subgoal orientated proof as at present, but at the end as well as being
able to rerun the proof you have just done it would also output the
tactic. Then you could do things like refer to assumptions by number
etc with the tactic recording system replacing the reference by the
actual assumption. 

Perhaps one of the things that hol2000 should have in mind is that it
would be the theorem prover core of a system with a (or perhaps a
variety of) user interface on top. Hence hol2000 does not itself need
to be majorly user friendly - but it needs to leave the hooks around so
that a user friendly interface can be built on top.

Ideas that other people have made about labelling assumptions etc
could be the sort of thing that could help here.

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."