The conversion BETA_CONV maps a beta-redex `(\x.u)v` to the theorem
|- (\x.u)v = u[v/x]
where u[v/x] denotes the result of substituting v for all free
occurrences of x in u, after renaming sufficient bound variables to avoid
variable capture. This conversion is one of the primitive inference rules of
the HOL system.
BETA_CONV tm fails if tm is not a beta-redex.
# BETA_CONV `(\x. x + 1) y`;;
val it : thm = |- (\x. x + 1) y = y + 1
# BETA_CONV `(\x y. x + y) y`;;
val it : thm = |- (\x y. x + y) y = (\y'. y + y')
The HOL Light primitive rule BETA is the special case where the argument is
the same as the bound variable. If you know that you are in this case, BETA
is significantly more efficient. Though traditionally a primitive, BETA_CONV
is actually a derived rule in HOL Light.