Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Sat, 15 Aug 92 12:42:02 EST
From: symdchon@au.edu.anu.mehta (donald syme )
Message-Id: <9208150242.AA10779@mehta>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: Rewriting with assumptions


Phil Weiss write:
> 
> I ran into an interesting problem the other day when rewriting.
> 
> I have a goal which looks something like this:
> 
> "A = B"
>   [ "B = C" ]
>   [ "D = C" ]
> I wanted to end up with "A = D"....

I haven't been using HOL long, but have often ended up with goals like
this (perhaps through using bad proof techniques?).  Anyway, as they 
are invariably frustrating, I wrote a very inefficient implementation
of "ELIMINATE_TAC".  The operation of this tactic was, given a variable
or term t to eliminate, look for an assumption of the form "t = ..." or
"... = t", UNDISCH_TAC all the other assumptions and perform the 
approprioate substitution, throwing the assumption away, thus eliminating
all the occurrences of the particular term from the goal and
assumptions.  It has proved so darn useful that I changed it to accept 
a list of terms and eliminate them all, or another version "TRY_ELIMINATE_TAC"
which attempts to perform the elimination on each term it is given.

Thus in the above problem, the required state "A = D" would be achieved by
ELIMINATE_TAC ["B";"C"].  Eliminating the B produces 
   "A = C"
      ["D = C"]

and eliminating the "C" produces just "A = D".

The inefficient (but functional) code for ELIMINATE_TAC follows.  The biggest
inefficiencies are in the number of UNDISCH_TAC and DISCH_TAC's involved,
and also in the setify/ASSUME operation done at the start to avoid the annoying
case where the assumption list has duplicates of assumptions.

   
let ELIMINATE_ONE_TAC t =
   POP_ASSUM_LIST (\thms_dupl.
      let thms = setify thms_dupl in
      EVERY (rev (map ASSUME_TAC thms))
   ) THEN
   POP_ASSUM_LIST (\thms.
      EVERY (map (\thm.
         let asm = snd (dest_thm thm) in 
         (\(asms,g).
            if (asms = []) & (is_eq asm) & ((fst(dest_eq asm) = t) or (snd(dest_
eq asm) = t))  then
               ASSUME_TAC thm (asms,g)
            else
               MP_TAC thm (asms,g)
         )
      ) thms) THEN
      POP_ASSUM (\asm.
         if (snd(dest_eq (snd (dest_thm asm))) = t) then
             SUBST1_TAC (SYM asm)
         else
             SUBST1_TAC asm
       )
       THEN EVERY (map (\t. DISCH_TAC) (tl thms))
   );;


let ELIMINATE_TAC L =
   EVERY (map ELIMINATE_ONE_TAC L);;
 
let TRY_ELIMINATE_TAC L =
   EVERY (map (\t. ELIMINATE_ONE_TAC t ORELSE ALL_TAC) L);;

 
Donald Syme,
Australian National University,
CANBERRA, 

symdchon@cs.anu.edu.au