Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 4 Jun 1993 11:15:19 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11263;
          Fri, 4 Jun 93 03:05:17 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from infix.cs.ruu.nl by ted.cs.uidaho.edu (16.6/1.34) id AA11258;
          Fri, 4 Jun 93 03:05:10 -0700
Received: by infix.cs.ruu.nl id AA11765 (5.65c/IDA-1.4.4 
          for info-hol@ted.cs.uidaho.edu); Fri, 4 Jun 1993 12:05:20 +0200
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
Message-Id: <199306041005.AA11765@infix.cs.ruu.nl>
Subject: REWRITING 2nd argument, how?
To: info-hol@ted.cs.uidaho.edu (hol mailing list)
Date: Fri, 4 Jun 1993 12:05:20 +0100 (METDST)
X-Mailer: ELM [version 2.4 PL21]
Content-Type: text
Content-Length: 544

Hi there,

Can anybody help me to write a tactic that does the following rewriting:

    * Given any goal of the form ?- REL trm1 trm2
    * Given a theorem th: |- trm2 = trm3
    * I want to rewrite the goal to get ?- REL trm1 trm3

the problem is that trm2 may be a subterm of trm1, so naive rewriting
will also rewrite trm1. The way I have in mind is to count the number
of occurrences of trm2 in REL trm1 trm2 then apply SUBST_OCCS_TAC to
the last occurence. Does someone know a more plausible way to do above
rwriting?

Thank you.

Wishnu