Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Message-Id: <9111012206.AA11341@ted.cs.uidaho.edu>
To: info-hol@edu.uidaho.cs.ted
In-Reply-To: Your message of "Fri, 01 Nov 91 13:26:07 MST." <9111012026.AA08557@fsa.cpsc.ucalgary.ca>
Date: Fri, 01 Nov 91 15:06:19 MST
From: jimaf@edu.uidaho.cs.ted

Graham writes:
> In summary,
>   if you want one assumption ASSUME it.
>   if you want several, take the lot and filter them
>                          via FILTER_ASM or via ASSUM_LIST

I agree with the first statement here in the context of this thread.
If we want to keep the proof readable then explicitly listing the assumptions
we are using via ASSUME or LET would be cnsistent with that desire.

Filtering an assumption list is almost as bad as numbering. Although it
allows proofs to be modified without worry of an explicit ordering on the
assumption list, it still does not "show" what assumptions we are using.

The problems I have come across in using ASSUME or LET arise in the type
arena. When proving lemmas about polymorphic types (which I do all the time)
it is much more difficult to use ASSUME than a number of an assumption.

If I could cut and paste the textual output of HOL and put it into an
ASSUME or LET without having to edit in all the type definitions, I would
be very happy, and things would be much easier -- although the proof code
would be longer.

-Jim Alves-Foss
(jimaf@ted.cs.uidaho.edu)   /* Of course these are MY opinions */
                            /* and may change without warning. */