1\DOC LIST_PBETA_CONV
2
3\TYPE {LIST_PBETA_CONV : conv}
4
5\KEYWORDS
6conversion.
7
8\LIBRARY
9pair
10
11\SYNOPSIS
12Performs an iterated paired beta-conversion.
13
14\DESCRIBE
15The conversion {LIST_PBETA_CONV} maps terms of the form
16{
17   (\p1 p2 ... pn. t) q1 q2 ... qn
18}
19to the theorems of the form
20{
21   |- (\p1 p2 ... pn. t) q1 q2 ... qn = t[q1/p1][q2/p2] ... [qn/pn]
22}
23where {t[qi/pi]} denotes the result of substituting {qi} for all free
24occurrences of {pi} in {t}, after renaming sufficient bound variables to avoid
25variable capture.
26
27\FAILURE
28{LIST_PBETA_CONV tm} fails if {tm} does not have the form
29{(\p1 ... pn. t) q1 ... qn} for {n} greater than 0.
30
31\EXAMPLE
32{
33- LIST_PBETA_CONV (Term `(\(a,b) (c,d) . a + b + c + d) (1,2) (3,4)`);
34> val it = |- (\(a,b) (c,d). a + b + c + d) (1,2) (3,4) = 1 + 2 + 3 + 4 : thm
35}
36
37
38\SEEALSO
39Drule.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.
40\ENDDOC
41