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: Tue, 18 Jul 95 10:15:35 +0100
Message-Id: <H00000cf00521c02@MHS>
In-Reply-To: <"9507180210.AA00696(a) mirtillo.usr.dsi.unimi.it *"@MHS>
Subject: easy HOL?
Mime-Version: 1.0
To: info-hol@leopard.cs.byu.edu
Cc: marco@mirtillo.usr.dsi.unimi.it
Content-Type: text/plain; charset=US-ASCII; name="Message text"
Content-Transfer-Encoding: 7bit

> While I.m not a master in the use of HOL, one of the most
> difficult things I found when I was learning how to develop
> a proof was assumptions management.
> 
> Theorem continuations, I think, are far too difficult to
> understand  when you are a beginner.
> 
> So I developed a couple of tactics which are easier to use,
> although they are very inefficent, and inelegant. The key
> idea is that who uses HOL knows natural deduction.
> 
> A natural way to develop a proof using natural deduction is
> to reason backward, i.e. try to reduce the goal formula to
> assumptions, or to reason backward, deducing something
> useful from assumptions.
> 
> The first case is easy implemented in HOL by means of tactics,
> while the second one is difficult, because we have no instruments
> to manipulate directly assumpitions.
> 
> We have the RULE_ASSUM_TAC which applies a gicen inference
> rule to all assumptions, but sometimes, a novice want to
> apply an inference rule to only one assumption.
> 
> The way to do this is easy: undischarge every assumption you don't
> need, and then apply the RULE_ASSUM_TAC properly, then, when
> you get the result, do a REPEAT STRIP_TAC to discharge what you
> can (usually the previously undischarged assumptions).

I sometimes use a similar type of tactic (which is actually a theorem
continuation!) which allows a given assumption to be extracted and
fed into a theorem taking tactic. Here it is in hol90 syntax (at least
I hope it is as I'm typing it in here and not testing it!)

fun USE_THEN tm ttac = (UNDISCH_TAC tm THEN DISCH_THEN ttac);

Note that the UNDISCH_BUT_TAC and UNDISCH_N_TAC while looking simple to use
can cause lots of grief later on as they depend on the explicit ordering of
assumptions in the goal - while you can normally get away with this there
this may be storing up trouble for the future as it is quite possible that
different versions of HOL (certainly hol88 vs hol90 I think but possibly also
different revisions of hol88) may add assumptions to the assumption list in
different orders. Relying on ordering of assumptions or rewrite rules etc etc
is always considered to be a "bad" thing.

-----------------------------------------------------------------------
                             david shepherd
SGS-THOMSON Microelectronics Ltd, 1000 aztec west, bristol bs12 4sq, UK
       tel/fax: +44 1454 611638/617910  email: des@bristol.st.com      
             www: http://www.inmos.co.uk/~des/welcome.html
     "whatever you don't want, you don't want negative advertising"