PAIRED_BETA_CONV : term -> thm

SYNOPSIS

Performs generalized beta conversion for tupled beta-redexes.

DESCRIPTION

The conversion PAIRED_BETA_CONV implements beta-reduction for certain applications of tupled lambda abstractions called `tupled beta-redexes'. Tupled lambda abstractions have the form `\.tm`, where is an arbitrarily-nested tuple of variables called a `varstruct'. For the purposes of PAIRED_BETA_CONV, the syntax of varstructs is given by:

     ::=   (v1,v2)  |  (,v)  |  (v,)  |  (,)

where v, v1, and v2 range over variables. A tupled beta-redex is an application of the form `(\.tm) t`, where the term `t` is a nested tuple of values having the same structure as the varstruct . For example, the term:

   `(\((a,b),(c,d)). a + b + c + d)  ((1,2),(3,4))`

is a tupled beta-redex, but the term:

   `(\((a,b),(c,d)). a + b + c + d)  ((1,2),p)`

is not, since p is not a pair of terms. Given a tupled beta-redex `(\.tm) t`, the conversion PAIRED_BETA_CONV performs generalized beta-reduction and returns the theorem

   |-  (\.tm) t = t[t1,...,tn/v1,...,vn]

where ti is the subterm of the tuple t that corresponds to the variable vi in the varstruct . In the simplest case, the varstruct is flat, as in the term:

   `(\(v1,...,vn).t) (t1,...,tn)`

When applied to a term of this form, PAIRED_BETA_CONV returns:

   |- (\(v1, ... ,vn).t) (t1, ... ,tn) = t[t1,...,tn/v1,...,vn]

As with ordinary beta-conversion, bound variables may be renamed to prevent free variable capture. That is, the term t[t1,...,tn/v1,...,vn] in this theorem is the result of substituting ti for vi in parallel in t, with suitable renaming of variables to prevent free variables in t1, ..., tn becoming bound in the result.

FAILURE CONDITIONS

PAIRED_BETA_CONV tm fails if tm is not a tupled beta-redex, as described above. Note that ordinary beta-redexes are specifically excluded: PAIRED_BETA_CONV fails when applied to `(\v.t)u`. For these beta-redexes, use BETA_CONV.

EXAMPLE

The following is a typical use of the conversion:

  # PAIRED_BETA_CONV `(\((a,b),(c,d)). a + b + c + d)  ((1,2),(3,4))`;;
  val it : thm = |- (\((a,b),c,d). a + b + c + d) ((1,2),3,4) = 1 + 2 + 3 + 4

Note that the term to which the tupled lambda abstraction is applied must have the same structure as the varstruct. For example, the following fail:

   # PAIRED_BETA_CONV `(\((a,b),p). a + b)  ((1,2),(3+5,4))`;;

   # PAIRED_BETA_CONV `(\((a,b),(c,d)). a + b + c + d)  ((1,2),p)`;;

because p is not a pair.