Return-Path: 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:50:06 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11276; Fri, 4 Jun 93 03:41:01 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from ganymede.inmos.co.uk by ted.cs.uidaho.edu (16.6/1.34) id AA11271; Fri, 4 Jun 93 03:40:51 -0700 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Fri, 4 Jun 93 11:41:00 BST From: David Shepherd Message-Id: <15540.9306041040@frogland.inmos.co.uk> Subject: Re: REWRITING 2nd argument, how? To: wishnu@cs.ruu.nl (Wishnu Prasetya) Date: Fri, 4 Jun 1993 11:40:38 +0100 (BST) Cc: info-hol@ted.cs.uidaho.edu In-Reply-To: <199306041005.AA11765@infix.cs.ruu.nl> from "Wishnu Prasetya" at Jun 4, 93 12:05:20 pm X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 973 Wishnu Prasetya has said: > 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? From Hol v2 onwards: CONV_TAC(RAND_CONV(REWRITE_CONV[th])) -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "They didn't like the rates, they don't like the poll tax, and they won't like the council tax." - Nicholas Ridley