Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
To: chou@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list), Tom.Melham@uk.ac.cam.cl
Subject: Re: Unnecessary renaming by BETA_CONV
In-Reply-To: Your message of Thu, 07 Jan 93 00:20:59 -0800. <9301070821.AA12631@maui.cs.ucla.edu>
Date: Sun, 10 Jan 93 23:59:21 +0000
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.552:10.01.93.23.59.31"@cl.cam.ac.uk>


chou@edu.ucla.cs asks:

> Dear HOL gurus:
> 
> Why does BETA_CONV perform the renaming shown below at all?
>
> ... [examples deleted] ...
> 
> ... But BETA_CONV is used
> at so many places and such a "feature" can cause unexpected
> behaviors in other proof procedures, one of which I encountered
> to my great annoyance.

The extra priming is due to the substitution primitive, subst,
which sometimes unecessarily renames bound variables.  For example:

   #let tm = subst ["n:num","m:num"] "!n:num. n = n";;
    tm = "!n'. n' = n'" : term

In theory, we *could* fix this. However messing with substitution 
is dangerous and it's probably best to leave it alone.

Whenever I've encountered this problam, I've managed to work
around it by employing "variant", genvars, etc.  See the attached
(old!) versions entry for an example.

Tom

+----------------------------------------------------------------------------+
| CHANGE TYPE:   Rewrite of prove_constructors_distinct			     |
|----------------------------------------------------------------------------|
| CHANGED BY:    TFM                                                         |
|----------------------------------------------------------------------------|
| FILES CHANGED: ml/tyfns.ml						     |
|----------------------------------------------------------------------------|
| DATE:          29 June 1990						     |
+----------------------------------------------------------------------------+

The built-in proof procedure:

    prove_constructors_distinct

has been largely rewritten.  Its code is now better structured and documented
and uses a slightly different algorithm.  The only difference in functionality
is that prove_constructors_distinct now returns a theorem without
unnecessarily primed variables.  

The change is best illustrated by an example.  If we define:

    let th = define_type 
    	     `five` `five = A num | B num | C num | D num | E num`;;

then executing the old version of prove_constructors_distinct:

   let old = prove_constructors_distinct th;;		% old version %

would return:

   old = |- (!n n'. ~(A n = B n')) /\
            (!n n''. ~(A n = C n'')) /\
            (!n n'''. ~(A n = D n''')) /\
            (!n n''''. ~(A n = E n'''')) /\
            (!n' n''. ~(B n' = C n'')) /\
            (!n' n'''. ~(B n' = D n''')) /\
            (!n' n''''. ~(B n' = E n'''')) /\
            (!n'' n'''. ~(C n'' = D n''')) /\
            (!n'' n''''. ~(C n'' = E n'''')) /\
            (!n''' n''''. ~(D n''' = E n''''))

Note the annoying extra "primes" on the n's.  The new implementation, on the
other hand, does less unnecessary priming.  Executing:

   let new = prove_constructors_distinct th;;		% new version %

will now return:

   new = |- (!n n'. ~(A n = B n')) /\
            (!n n'. ~(A n = C n')) /\
            (!n n'. ~(A n = D n')) /\
            (!n n'. ~(A n = E n')) /\
            (!n n'. ~(B n = C n')) /\
            (!n n'. ~(B n = D n')) /\
            (!n n'. ~(B n = E n')) /\
            (!n n'. ~(C n = D n')) /\
            (!n n'. ~(C n = E n')) /\
            (!n n'. ~(D n = E n'))

Users may be interested to note that the unnecessary priming was due to the 
following behaviour of the primitive operation "subst":

   #let tm = subst ["n:num","m:num"] "!n:num. n = n";;
   tm = "!n'. n' = n'" : term

Note that the n gets unnecessarily primed.