----------------------------------------------------------------------
GEN_ALPHA_CONV                                                 (Drule)
----------------------------------------------------------------------
GEN_ALPHA_CONV : term -> conv

SYNOPSIS
Renames the bound variable of an abstraction, a quantified term, or other
binder application.

KEYWORDS
conversion, alpha.

DESCRIBE
The conversion {GEN_ALPHA_CONV} provides alpha conversion for lambda
abstractions of the form {\y.t}, quantified terms of the forms {!y.t},
{?y.t} or {?!y.t}, and epsilon terms of the form {@y.t}.  In general,
if {B} is a binder constant, then {GEN_ALPHA_CONV} implements alpha
conversion for applications of the form {B y.t}.

If {tm} is an abstraction {\y.t} or an application of a binder to
an abstraction {B y.t}, where the bound variable {y} has type {ty},
and if {x} is a variable also of type {ty}, then {GEN_ALPHA_CONV x tm}
returns one of the theorems:

   |- (\y.t)  = (\x'. t[x'/y])
   |- (B y.t)  = (B x'. t[x'/y])

depending on whether the input term is {\y.t} or {B y.t}
respectively.  The variable {x':ty} in the resulting theorem is a primed
variant of {x} chosen so as not to be free in the term provided as the second
argument to {GEN_ALPHA_CONV}.

FAILURE
{GEN_ALPHA_CONV x tm} fails if {x} is not a variable, or if {tm} does not have
one of the forms {\y.t} or {B y.t}, where {B} is a binder.
{GEN_ALPHA_CONV x tm} also fails if {tm} does have one of these
forms, but types of the variables {x} and {y} differ.

SEEALSO
Thm.ALPHA, Drule.ALPHA_CONV, boolSyntax.new_binder_definition.

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