Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: weiss@edu.uidaho.cs.leopard (Phil Weiss)
Message-Id: <9208141835.AA16901@leopard.cs.uidaho.edu>
Subject: Rewriting with assumptions
To: info-hol@edu.uidaho.cs.ted (HOL Mailing List)
Date: Fri, 14 Aug 92 11:35:49 PDT
Mailer: Elm [revision: 66.33]

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".  So I did ASM_REWRITE_TAC
and got "A = C" and then used 

POP_ASSUM_LIST (\thl. REWRITE_TAC
	(map (CONV_RULE (ONCE_DEPTH_CONV SYM_CONV)) thl));;

to replace the C with the D.  Only since "B = C" is listed
first in the assumptions, I end up with "A = B" again.

I tried with some success to use FILTER_ASM_REWRITE_TAC but that
got complicated.  After some playing around, I wrote this tactic.

let ASM_REMOVE_REWRITE_TAC =
POP_ASSUM_LIST
 (\thl. MAP_EVERY (\th. (\g.
  (CHANGED_TAC (REWRITE_TAC [th] g)) ? (ASSUME_TAC th g)))
  thl)
;;

which rewrites the goal, removing any theorems used in the rewriting.
Then I can rewrite using the SYM_CONV dealie no problem.

Has anyone else encountered this problem?  Have you found any better
solutions?  I'm not too fond of mine, as it only rewrites one
assumption at a time.

Phil.
--
Philip Weiss	Laboratory for Applied Logic	weiss@leopard.cs.uidaho.edu
(Disclaimer: My views are not their views)	weiss872@snake.cs.uidaho.edu