Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Message-Id: <9201241505.AA00515@easynet.crl.dec.com>
Date: Fri, 24 Jan 92 10:05:26 EST
From: "Tim Leonard, Cantab. 24-Jan-1992 1005" <leonard@com.dec.enet.ricks>
To: info-hol@edu.uidaho.cs.ted
Apparently-To: info-hol@ted.cs.uidaho.edu
Subject: Re: referring to assumptions cont'ed

I watched with interest the discussion about referring to assumptions.  Here
are two functions I use, which let me update old proofs with the least work, by
producing an ordered list of the assumptions I care about.  The second function
also throws away any assumptions that are no longer needed.

Tim


%
-------------------------------------------------------------------------------
We define a function to allow assumptions to be named.  The first operand is a
list of terms, each of which identifies an assumption in the assumption list.
The function produces a list of assumptions in the order they were identified,
and passes that to function that produces a tactic, and applies the tactic.
-------------------------------------------------------------------------------
%
let GET_ASSUMPTIONS
    (terms: term list)
    (f: thm list -> tactic)
    (asms, conc) =
% If some terms aren't already assumptions, report that there's a problem. %
  let bad_term (tm: term) = not (exists (aconv tm) asms) in
    if exists bad_term terms
    then failwith `GET_ASSUMPTIONS --- some term isn't an assumption.`;
% Two terms correspond if they're identical after renaming. %
  let corresponds asm tm = aconv tm asm in
% Create the list of assumptions identified by the given terms. %
  let thms = map ASSUME terms in
% Create a tactic with the identified assumptions, and apply it. %
  f thms (asms, conc);;


%
-------------------------------------------------------------------------------
We define a function to allow assumptions to be named (and selectively popped).
The first operand is a list of pairs, where the first element of each pair is a
term that identifies an assumption in the assumption list, and the second
element is a boolean saying whether that assumption should be kept.  The second
operand is another bool saying whether to keep all the assumptions that aren't
identified by any term in the list.  The function produces an list of
assumptions in the order they were identified, and passes that to function that
produces a tactic, which is then applied to the filtered hypotheses.
-------------------------------------------------------------------------------
%

let GET_AND_POP_ASSUMPTIONS
    (pairs: (term # bool) list)
    (default: bool)
    (f: thm list -> tactic)
    (asms, conc) =
% If there are any bad pairs, report that there's a problem. %
  let bad_pair (tm: term, keep: bool) = not (exists (aconv tm) asms) in
    if exists bad_pair pairs
    then failwith `GET_AND_POP_ASSUMPTIONS --- some term isn't an assumption.`;
% Two terms correspond if they're identical after renaming. %
  let corresponds asm pair = aconv (fst pair) asm in
% If an assumption has a pair, do what it says; otherwise, do the default. %
  let should_keep asm = snd (find (corresponds asm) pairs) ? default in
% Create the set of assumptions to keep. %
  let asms' = filter should_keep asms in
% Create the list of assumptions identified by the given terms. %
  let thms = map ASSUME (fst (split pairs)) in
% Create a tactic with the identified asms, and apply it to the kept asms. %
  f thms (asms', conc);;