LIST_PBETA_CONV : conv
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Performs an iterated paired beta-conversion.
DESCRIPTION
The conversion LIST_PBETA_CONV maps terms of the form 
   (\p1 p2 ... pn. t) q1 q2 ... qn
to the theorems of the form 
   |- (\p1 p2 ... pn. t) q1 q2 ... qn = t[q1/p1][q2/p2] ... [qn/pn]
where t[qi/pi] denotes the result of substituting qi for all free occurrences of pi in t, after renaming sufficient bound variables to avoid variable capture.
FAILURE
LIST_PBETA_CONV tm fails if tm does not have the form (\p1 ... pn. t) q1 ... qn for n greater than 0.
EXAMPLE
- LIST_PBETA_CONV (Term `(\(a,b) (c,d) . a + b + c + d) (1,2) (3,4)`);
> val it = |- (\(a,b) (c,d). a + b + c + d) (1,2) (3,4) = 1 + 2 + 3 + 4 : thm

SEEALSO
LIST_BETA_CONV, PBETA_CONV, BETA_RULE, BETA_TAC, RIGHT_PBETA, RIGHT_LIST_PBETA, LEFT_PBETA, LEFT_LIST_PBETA
HOL  Kananaskis-14