GEN_ALPHA_CONV
Drule.GEN_ALPHA_CONV : term -> conv
Renames the bound variable of an abstraction, a quantified term, or other binder application.
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.
See also
Thm.ALPHA, Drule.ALPHA_CONV,
boolSyntax.new_binder_definition