Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: tfm@dcs.gla.ac.uk
Message-Id: <9408170814.AA09791@switha.dcs.gla.ac.uk>
To: shaw@cs.ucdavis.edu (Rob Shaw)
Cc: info-hol@cs.uidaho.edu, tfm@dcs.gla.ac.uk
Subject: Re: Why the genvar's ?
In-Reply-To: Your message of "Tue, 16 Aug 94 12:34:59 PDT." <9408161934.AA21851@ice.cs.ucdavis.edu>
Date: Wed, 17 Aug 94 09:14:21 +0100

Rob Shaw asks about rewriting a goal

>   "F"
>      2  ["y <= x" ]
>      1  ["x < y" ]

with

> [*]    |- F = x < y /\ y <= x

resulting in 

> "GEN%VAR%557 < GEN%VAR%558 /\ GEN%VAR%558 <= GEN%VAR%557"
>   2  ["y <= x" ]
>   1  ["x < y" ]
> 
> Why don't I get the new goal "(x < y) /\ (y <= x)" ?

It's because x and y are free on the right-hand side of [*] but not
on the left.  Hence, since x and y can be anything, the system picks
(using genvar) variables guaranteed not to clash with anything in the 
current context -- whatever that might be.  So, for example, one could 
also rewrite

  "!x y. F"

and be sure the rewrite is not blocked by capture problems.

For full details, see the REFERENCE entry for REWR_CONV, which says:

> This situation is, however, relatively rare; in most equations the free
> variables on the right-hand side are a subset of the free variables on the
> left-hand side.

Actually, this is what *should* be true -- if you are finding yourself in
a situation in which it isn't, then it might be a good idea to have another
look at your proof.

Tom