Date: Tue, 13 Aug 91 09:28:29 +0200
From: kimdam@dk.tfl.sun
Subject: Re: Alphabetic change of bound variables
To: info-hol@edu.ucdavis.eecs.iris
Message-Id: <9108130728.AA18893@ux6.tfl.dk>


>
> How is that handled (1) in the HOL logic and (2) in the HOL system?  I can't
> find any mention of the subject in the documentation.
>
> Garrel Pottinger
> garrel@oracorp.com
>

(1) Alpha convertible terms are considered equivalent (the _exact_ same),
    in the HOL logic.

(2) This also holds for the HOL system.  An explicit prove of the
    equality of two HOL term, e.g. proving:

        |- tm1 = tm2

    where tm1 and tm2 are alpha convertible, may be done using the rule
    below:

    let ALPHA_EQ tm1 tm2 =
      let thm1 = DISCH (mk_eq(tm1,tm1)) (ASSUME(mk_eq(tm1,tm2))) and
          thm2 = REFL tm1
      in
        MP thm1 thm2;;

    In this rule DISCH is applied with "tm1 = tm1", but actually
    discharges the assumed alpha-convertible term: "tm1 = tm2"

    The rule may be called like:

        ALPHA_EQ "\x:bool.x" "\y:bool.y"  -->  |- (\x.x) = (\y.y)

    Combining the rule above with EQ_MP like:

    let ALPHA_MP tm thm =
      let thm1 = ALPHA_EQ (concl thm) tm
      in
        EQ_MP thm1 thm;;

    yields a rule for transforming a theorem into an alpha-convertible
    theorem:

       ALPHA_MP "T = ((\y:bool.y) = (\w.w))" T_DEF -->
          |- T = ((\y.y) = (\w.w))

Kind Regards
        Kim Dam Petersen        (E-mail: kimdam@tfl.dk)