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.
FAILURE
BETA_CONV tm fails if tm is not a beta-redex.
EXAMPLE
- BETA_CONV (Term `(\x.x+1)y`);
> val it = |- (\x. x + 1)y = y + 1 :thm
- BETA_CONV (Term `(\x y. x+y)y`);
> val it = |- (\x y. x + y)y = (\y'. y + y') : thm