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:52:29 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11283; Fri, 4 Jun 93 03:43:10 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA11278; Fri, 4 Jun 93 03:42:59 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 4 Jun 1993 11:42:25 +0100 To: Wishnu Prasetya Cc: info-hol@ted.cs.uidaho.edu (hol mailing list), Tom.Melham@cl.cam.ac.uk Subject: Re: REWRITING 2nd argument, how? In-Reply-To: Your message of "Fri, 04 Jun 93 12:05:20 BST." <199306041005.AA11765@infix.cs.ruu.nl> Date: Fri, 04 Jun 93 11:42:17 +0100 From: Tom Melham Message-Id: <"swan.cl.cam.:033150:930604104241"@cl.cam.ac.uk> Wishnu Prasetya asks for a tactic such that: > * 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 A simple way to do this is to use a conversion. Here is an example: #g "1 + 0 = 1";; "1 + 0 = 1" () : void #let th = num_CONV "1";; th = |- 1 = SUC 0 #expand(CONV_TAC (RAND_CONV (REWR_CONV th)));; OK.. "1 + 0 = SUC 0" () : void The conversion c = (REWR_CONV |- trm2 = trm3) maps the term trm2 to the theorem |- trm2 = trm3. The conversion RAND_CONV c then applies the conversion c to the "rand" (or operand) of a term, which for terms of the form "REL trm1 trm2" means the subterm trm2. Finally, CONV_TAC converts this into a tactic. Of course, REWR_CONV does actual rewriting (i.e. substitution with instantiation) rather than plain substitution. More elaborate tactics in the same spirit are also possible. For example CONV_TAC (RAND_CONV (REWRITE_CONV th)) will (among other things) rewrite subterms of trm2. Judicious combinations of RAND_CONV, ABS_CONV, and RATOR_CONV will let you get at any selected subterm. Tom