Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
To: garrel@com.oracorp
Cc: info-hol@edu.uidaho.cs.ted
Subject: Selecting assumptions
Date: Thu, 31 Oct 91 17:17:09 +0000
From: John.Harrison@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.010:31.09.91.17.17.14"@cl.cam.ac.uk>


Perhaps Wim should have mentioned in his dire warning how to use
particular assumptions *without* selecting them by number...

1. One reasonable way is just to use

     ASSUME "xxxxx"

   where "xxxxx" is the relevant assumption, wherever you need to
   use that particular theorem. For example:

     SUBST1_TAC(ASSUME "x = v + 2")

   In general, you can use a theorem with any assumptions you like
   in a backward proof, but its assumptions must be a subset of the
   goal's assumptions, or the tactic resulting will not be valid.

   The main defects of this approach are:

     (a) It can become rather verbose

     (b) It depends on the particular variable names in the assumption,
         which may be as they are owing to automatic renaming, or
         the particular variable names used in lemmas. (This can be
         ameliorated by using X_... versions of some functions, e.g.
         X_CHOOSE_TAC or X_FUN_EQ_CONV.)

2. If you have only one assumption, then POP_ASSUM is quite safe:

     POP_ASSUM SUBST1_TAC

   Although this loses the assumption afterwards. You could try

     W(SUBST1_TAC o ASSUME o hd o fst)

   or some such hack instead.

3. The most flexible way is to use FIRST_ASSUM, or some nonce tactic
   of your own devising, to select the assumption according to its
   structure. The tactic

     FIRST_ASSUM ttac

   applies the theorem-tactic ttac to the first (ASSUMEd) assumption
   on which it succeeds and the resulting tactic succeeds when
   applied to the goal. (N.B. The example below uses SUBST1_TAC, which
   never fails on the goal, but will fail when given a non-equation.)
   Therefore

     FIRST_ASSUM SUBST1_TAC

   will substitute with the first equational assumption, while

     FIRST_ASSUM (SUBST1_TAC o SYM)

   will substitute backwards with the same assumption. Note that this
   should only be used when ttac can only succeed on one assumption,
   otherwise a dependency on ordering is again introduced. You can
   artificially restrict the applicability of the theorem-tactic
   to make sure this is the case, e.g.

     FIRST_ASSUM(SUBST1_TAC o assert (curry$= "x:num" o lhs o concl))

   will substitute with the first equational assumption whose LHS is
   "x:num". Arbitrarily complex selections can be made in the same
   manner.

4. Ideally, you should try to avoid creating unnecessary assumptions,
   by careful use of theorem-tactics. This can be tricky on very intricate
   hardware theorems, but there are many cases where it is easy, e.g.

      DISCH_THEN SUBST_ALL_TAC

   will undischarge and substitute with the antecedent of an implication
   in both the assumptions and conclusion of a goal.

I hope one of these methods will be suitable for the case you have in hand.

==============================================================================
John Harrison (jrh@cl.cam.ac.uk)

Hardware Verification Group
University of Cambridge Computer Laboratory
New Museums Site
Pembroke Street
Cambridge CB2 3QG
England.
==============================================================================