LIST_BETA_CONV : conv
STRUCTURE
Drule
SYNOPSIS
Performs an iterated beta conversion.
DESCRIPTION
The conversion LIST_BETA_CONV maps terms of the form 
   "(\x1 x2 ... xn. u) v1 v2 ... vn"
to the theorems of the form 
   |- (\x1 x2 ... xn. u) v1 v2 ... vn = u[v1/x1][v2/x2] ... [vn/xn]
where u[vi/xi] denotes the result of substituting vi for all free occurrences of xi in u, after renaming sufficient bound variables to avoid variable capture.
FAILURE
LIST_BETA_CONV tm fails if tm does not have the form "(\x1 ... xn. u) v1 ... vn" for n greater than 0.
EXAMPLE
- LIST_BETA_CONV (Term `(\x y. x+y) 1 2`);
> val it = |- (\x y. x + y)1 2 = 1 + 2 : thm

SEEALSO
BETA_CONV, BETA_RULE, BETA_TAC, RIGHT_BETA, RIGHT_LIST_BETA
HOL  Trindemossen-1