LIST_BETA_CONV
Drule.LIST_BETA_CONV : conv
Performs an iterated beta conversion.
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
See also
Thm.BETA_CONV, Conv.BETA_RULE,
Tactic.BETA_TAC,
Drule.RIGHT_BETA,
Drule.RIGHT_LIST_BETA