PairRules.PBETA

STRUCTURE

SYNOPSIS

Performs a general beta-conversion.

DESCRIPTION

The conversion PBETA_CONV maps a paired beta-redex "(\p.t)q" to the theorem

   |- (\p.t)q = t[q/p]

where u[q/p] denotes the result of substituting q for all free occurrences of p in t, after renaming sufficient bound variables to avoid variable capture. Unlike PAIRED_BETA_CONV, PBETA_CONV does not require that the structure of the argument match the structure of the pair bound by the abstraction. However, if the structure of the argument does match the structure of the pair bound by the abstraction, then PAIRED_BETA_CONV will do the job much faster.

FAILURE

PBETA_CONV tm fails if tm is not a paired beta-redex.

EXAMPLE

PBETA_CONV will reduce applications with arbitrary structure.

   - PBETA_CONV 
        (Term `((\((a:'a,b:'a),(c:'a,d:'a)). f a b c d) ((w,x),(y,z))):'a`);
   > val it = |- (\((a,b),c,d). f a b c d) ((w,x),y,z) = f w x y z : thm

PBETA_CONV does not require the structure of the argument and the bound pair to match.

   - PBETA_CONV 
       (Term `((\((a:'a,b:'a),(c:'a,d:'a)). f a b c d) ((w,x),yz)):'a`);
   > val it = |- (\((a,b),c,d). f a b c d) ((w,x),yz) = 
                 f w x (FST yz) (SND yz) : thm

PBETA_CONV regards component pairs of the bound pair as variables in their own right and preserves structure accordingly:

   - PBETA_CONV 
       (Term `((\((a:'a,b:'a),(c:'a,d:'a)). f (a,b) (c,d)) (wx,(y,z))):'a`);
   > val it = |- (\((a,b),c,d). f (a,b) (c,d)) (wx,y,z) = f wx (y,z) : thm

SEEALSO

BETA_CONV, PAIRED_BETA_CONV, PBETA_RULE, PBETA_TAC, LIST_PBETA_CONV, RIGHT_PBETA, RIGHT_LIST_PBETA, LEFT_PBETA, LEFT_LIST_PBETA