Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <24649-0@swan.cl.cam.ac.uk>; Thu, 13 Aug 1992 10:18:57 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28652; Thu, 13 Aug 92 02:09:42 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA28647; Thu, 13 Aug 92 02:09:35 -0700 Received: from cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <24315-0@swan.cl.cam.ac.uk>; Thu, 13 Aug 1992 10:05:29 +0100 To: Phil Windley , info-hol@edu.uidaho.cs.ted Cc: Wai Wong Subject: Re: Conditional rewriting In-Reply-To: Your message of Wed, 12 Aug 92 20:44:07 -0700. <199208130344.AA06433@panther.cs.uidaho.edu> Date: Thu, 13 Aug 92 10:05:08 +0100 From: Wai Wong Message-Id: <"swan.cl.ca.334:13.07.92.09.06.00"@cl.cam.ac.uk> On Wed, 12 Aug 92 20:44:07 Phil wrote: > I think, however, that conditional rewriting is sufficiently important that > it should be built into the basic HOL system so that beginners can use it > from the beginning. Having conditional rewriting positively affects one > proof style IMHO. I entirely agree with Phil. I think a mininium set of conditional rewriting tools should be built in the basic HOL system. This will help both beginners and more experienced users. The code I sent a couple days ago does the following: A ?- t[u'] ====================== COND_REWRITE_TAC |- !x. P[x] ==> (u[x] = v[x]) A,P ?- t[v'] A ?- P or A,P ?- t[u'] =================== COND_REWRITE_TAC |- !x. P[x] ==> (u[x] = v[x]) A,P ?- t[v'] Are there any suggestions what should be in the mininium set of useful conditional rewriting tools? If we can come up with some agreement, someone, or perhaps me, can put it into the system. By the way, thanks to several people who pointed out there is some conditional rewriting tools under the `contrib' directory. Wai