APPLY rules and PAIR[x, y]

Johan G. F. Belinfante
2008 September 8

SetDirectory["l:"];  <<  goedel.08sep07a; << tools.m

summary

A formula for PAIR[x,y] is derived which makes it easy to derive APPLY rules for binary functions.

introduction

For some binary functions there may only be available an APPLY rule involving PAIR.  For example:

APPLY[NATEXP, PAIR[x, y]]

APPLY[NATEXP, x]

All three Normality tests fail to provide anything useful, and ApComp yields the following true but useless result.

ApComp[NATEXP, id[cart[V, V]], x]

In this notebook a new rewrite rule for PAIR[x, y] is derived that allows one to obtain a more useful result.  The following result obtained using Normality helps motivate the new result.

PAIR[first[x], second[x]] // Normality

Further motivation comes from this formula:

APPLY[id[cart[V, V]], x]

a new formula for PAIR

The derivation of the new formula is an example of a situation in which the GOEDEL program knows a fact to be true, but lacks a corresponding rewrite rule.  One simply has to ask the right question!  The motivating examples in the preceding section provided a clue that led to asking the right question as it were.

Theorem.

equal[union[x, complement[image[V, set[first[x]]]]], 
      PAIR[first[x], second[x]]]

union[x_, complement[image[V, set[first[x_]]]]] := 
      PAIR[first[x], second[x]]

With this new rewrite rule in place, the use of ApComp allows one to derive general APPLY rules for binary functions when special APPLY rules involving PAIR are available.  The next section provides some examples.

applications

Theorem.

ApComp[INTMUL, id[cart[V, V]], x] // Reverse

APPLY[INTMUL, x_] := intmul[first[x], second[x]]

Theorem.

ApComp[MIXMUL, id[cart[V, V]], x] // Reverse

APPLY[MIXMUL, x_] := intmul[first[x], plus[second[x]]]

Theorem.

ApComp[NATEXP, id[cart[V, V]], x] // Reverse

APPLY[NATEXP, x_] := natexp[first[x], second[x]]