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); Tue, 26 Jan 1993 07:29:23 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02067;
          Mon, 25 Jan 93 23:20:23 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA02062;
          Mon, 25 Jan 93 23:20:17 -0800
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA04034;
          Mon, 25 Jan 93 23:19:46 -0800
Message-Id: <9301260719.AA04034@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list)
Subject: REWRITE_TAC vs SUBST1_TAC
Date: Mon, 25 Jan 93 23:19:42 PST
From: chou@edu.ucla.cs

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?

Notice that if the bound variable is "y" instead of "x",
both REWRITE_TAC and SUBST1_TAC work:

    #set_goal([ ], "(x' = x + 1) ==> (!y. (y + x') > y)");;
    "(x' = x + 1) ==> (!y. (y + x') > y)"
    

    #e(DISCH_THEN (\th. REWRITE_TAC [th]));;
    OK..
    "!y. (y + (x + 1)) > y"
    

    #b();;
    "(x' = x + 1) ==> (!y. (y + x') > y)"
    

    #e(DISCH_THEN (SUBST1_TAC));;
    OK..
    "!y. (y + (x + 1)) > y"

- Ching Tsun