Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <18079-0@swan.cl.cam.ac.uk>; Tue, 11 Aug 1992 09:57:08 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA25991;
          Tue, 11 Aug 92 01:47:27 -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 AA25986;
          Tue, 11 Aug 92 01:47:20 -0700
Received: from cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl 
          id <17633-0@swan.cl.cam.ac.uk>; Tue, 11 Aug 1992 09:33:43 +0100
To: info-hol@edu.uidaho.cs.ted
Subject: Conditional rewriting
Date: Tue, 11 Aug 92 09:33:30 +0100
From: Wai Wong <Wai.Wong@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.639:11.07.92.08.34.00"@cl.cam.ac.uk>

Has anyone had a tactic which does conditional rewriting?
By this I mean it perform something like:

  A ?- t[u']
 ============ COND_REWRITE_TAC |- P ==> (u = v)
  A ?- t[v']

if P is in A, otherwise,

  A ?- t[u']
 ======================= COND_REWRITE_TAC |- P ==> (u = v)
  A,P ?- t[v']  A ?- P

where u' mathces u and the (first) subgoal is the result of
rewriting using the conclusion of the input theorem.

Wai