----------------------------------------------------------------------
PALPHA                                                     (PairRules)
----------------------------------------------------------------------
PALPHA : term -> term -> thm

KEYWORDS
rule, alpha.

LIBRARY
pair

SYNOPSIS
Proves equality of paired alpha-equivalent terms.

DESCRIBE
When applied to a pair of terms {t1} and {t1'} which are
alpha-equivalent, {ALPHA} returns the theorem {|- t1 = t1'}.


   -------------  PALPHA "t1" "t1'"
    |- t1 = t1'


The difference between {PALPHA} and {ALPHA} is that
{PALPHA} is prepared to consider pair structures of different
structure to be alpha-equivalent.
In its most trivial case this means that {PALPHA} can consider
a variable and a pair to alpha-equivalent.

FAILURE
Fails unless the terms provided are alpha-equivalent.

EXAMPLE

- PALPHA (Term `\(x:'a,y:'a). (x,y)`) (Term`\xy:'a#'a. xy`);
> val it = |- (\(x,y). (x,y)) = (\xy. xy) : thm




COMMENTS
Alpha-converting a paired abstraction to a nonpaired abstraction
can introduce instances of the terms {FST} and {SND}.
A paired abstraction and a nonpaired abstraction will be considered
equivalent by {PALPHA} if the nonpaired abstraction contains all
those instances of {FST} and {SND} present in the paired
abstraction, plus the minimum additional instances of {FST} and {SND}.
For example:

   - PALPHA
      (Term `\(x:'a,y:'b). (f x y (x,y)):'c`)
      (Term `\xy:'a#'b. (f (FST xy) (SND xy) xy):'c`);
   > val it = |- (\(x,y). f x y (x,y)) = (\xy. f (FST xy) (SND xy) xy) : thm

   - PALPHA
      (Term `\(x:'a,y:'b). (f x y (x,y)):'c`)
      (Term `\xy:'a#'b. (f (FST xy) (SND xy) (FST xy, SND xy)):'c`)
     handle e => Raise e;

   Exception raised at ??.failwith:
   PALPHA
   ! Uncaught exception:
   ! HOL_ERR




SEEALSO
Thm.ALPHA, Term.aconv, PairRules.PALPHA_CONV,
PairRules.GEN_PALPHA_CONV.

----------------------------------------------------------------------