Date: Fri, 1 Nov 91 10:11:43 +0100
From: kimdam%ux5.BITNET@edu.cuny.cunyvm
Subject: X_POP_ASSUM
To: info-hol@edu.ucdavis.eecs.iris
Message-Id: <9111010911.AA09485@ux5.tfl.dk>

A couple of years ago I made a simple variant of POP_ASSUM, called
X_POP_ASSUM, which might be of use to other HOL users.

The tactic may be used for popping an explicitly named assumption.  It
takes two arguments: an assumption to be popped and a theorem-tactic.
The assumption popped off is fed to the theorem-tactic, and the
resulting tactic is then applied to the original goal, with the
specified assumption stripped off.

To reduce typing errors I usually copy the assumption from the HOL
output, and supply some proper types.

In the cases where I want to use an assumption in a tactic, without
popping it, I simply use (ASSUME asm) to thm-ize the assumption in the
tactic.

Regards
    Med k{\ae}rlig Hilsen,

        Kim Dam Petersen        (Email: kimdam@tfl.dk)

% --------------------------------------------------------------------------- %
%<
        X_POP_ASSUM asm f

        A u [asm] ?- t
        ==============
        f asm (A ?- t)
>%
let X_POP_ASSUM (asm:term) (f:thm_tactic) (hyp,conc) =
  let hyp' = filter (\asm'. not(aconv asm asm')) hyp in
  if hyp' = hyp then
    failwith `X_POP_ASSUM`
  else
    f(ASSUME asm)(hyp', conc);;