LIST_PBETA_CONV

PairRules.LIST_PBETA_CONV : conv

Performs an iterated paired beta-conversion.

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

See also

Drule.LIST_BETA_CONV, PairRules.PBETA_CONV, Conv.BETA_RULE, Tactic.BETA_TAC, PairRules.RIGHT_PBETA, PairRules.RIGHT_LIST_PBETA, PairRules.LEFT_PBETA, PairRules.LEFT_LIST_PBETA