Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Message-Id: <199110312356.AA05176@panther.cs.uidaho.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: referring to assumptions cont'ed
In-Reply-To: Your message of Thu, 31 Oct 91 21:42:52 -0100. <9110312242.AA06641@esat.kuleuven.ac.be>
Date: Thu, 31 Oct 91 15:56:17 -0800
From: Phil Windley <windley@edu.uidaho.cs.panther>

On Thu, 31 Oct 91 21:42:52 -0100, Wim Ploegaer wrote:

+------------
| You can conclude from this that using the explicit order of the
| assumptions will only cause problems if the behavior of some basic
| mechanims changes. But, as the manual clearly states that the
| assumptions form a *set*, this kind of changes might occur again in
| some later version of HOL. Thus, if you want to write code that lasts
| for a while, you should bare this in mind.

While I agree in general that one should not use the order of assumptions
in a proof, I must say that its is A LOT more work.  This is why its so
easy to fall into the trap.

In my later years, I've managed to write some stuff that made it through
all the recent changes in the HOL system (except for the RES_TAC stuff) and
was quite proud of that, but it isn't the proof style that I find most
natural.  When the pressure's on, I still am liable to start counting
assumptions.

Some of the difficulty, I think, is that its hard to get (short of reading
the HOL system itself) a good feel for how to do things.  For example, I've
been using HOL for 4 years now and John Harrison's suggestion to use

   SUBST1_TAC ASSUME "x = ..."

was something I'd never thought of.  Its obvious now, but ...

Next time you do something really clever, post it to info-hol.  I promise
that there are a lot of things that may seem trivial, but are real eye
openers to others.

--phil--