Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4); Wed, 27 Jan 1993 13:20:25 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07767;
          Wed, 27 Jan 93 04:51:37 -0800
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 AA07762;
          Wed, 27 Jan 93 04:51:27 -0800
Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Wed, 27 Jan 1993 12:49:39 +0000
To: chou@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list), Tom.Melham@uk.ac.cam.cl
Subject: Re: REWRITE_TAC vs SUBST1_TAC
In-Reply-To: Your message of Mon, 25 Jan 93 23:19:42 -0800. <9301260719.AA04034@maui.cs.ucla.edu>
Date: Wed, 27 Jan 93 12:49:25 +0000
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.674:27.01.93.12.49.48"@cl.cam.ac.uk>


Ching Tsun (chou@edu.ucla.cs) asks:

> Consider the following HOL session:
> 
>     #set_goal([ ], "(x' = x + 1) ==> (!x. (x + x') > x)");;
>     "(x' = x + 1) ==> (!x. (x + x') > x)"
>     
> 
>     #e(DISCH_THEN (\th. REWRITE_TAC [th]));;
>     OK..
>     "!x. (x + x') > x"
>     
> 
>     #b();;
>     "(x' = x + 1) ==> (!x. (x + x') > x)"
>     
> 
>     #e(DISCH_THEN (SUBST1_TAC));;
>     OK..
>     "!x'. (x' + (x + 1)) > x'"
> 
> Why does REWRITE_TAC fail to substitute "x + 1" for "x'",
> while SUBST1_TAC succeeds in doing so?


This is a long-standing feature/bug arising as a consequence of HOL's
conversion-based rewriting implementation.  What happens is that the term

    "!x. (x + x') > x"

is being rewritten with the theorem

    x' = x + 1 |- x' = x + 1

The underlying process of conversion manages to create the partial result

    x' = x + 1 |- ((x + x') > x) = ((x + (x + 1)) > x)

but failure then occurs at this stage when the system tries to generalize
over x to complete the reconstruction of the original term (because x is
free in the hypotheses).  The trouble is that the implementation is not
clever enough to rename the variable x.

I've looked briefly at fixing this problem (and some related ones), but I
haven't yet found an implementation that's fast enough...  

Tom