Lambda the Ultimate

Has there been a paper describing optimizations to arithmetic for tagged pointer representations? For instance, stealing 1-bit to distinguish pointers and integers, and using 0 as the tag value for integers, we don't need to perform any shifting for integer addition in order to normalize the integer back to its tagged representation:

-- integer i is represented as a word shifted by 1 bit:
-- word = tag(int)
tag(int) = int << 2
         = word * 2

-- int = untag(word)
untag(word) = word >> 2
            = word / 2

-- no shift needed; subtraction the same
addition = int0 + int1
         = tag( untag(word0) + untag(word0) )
         = tag( (word0 / 2) + (word1 / 2) )
         = tag( (word0 + word1) / 2)
         = 2 * (word0 + word1) / 2
         = word0 + word1

-- one right shift needed to normalize
multiplication = int0 * int1
               = tag( untag(word0) * untag(word1) )
               = tag( (word0 / 2) * (word1 / 2) )
               = tag( word0 * word1 / 4 )
               = 2 * word0 * word1 / 4
               = word0 * word1 / 2

-- one left shift needed to normalize
division = int0 / int1
         = tag( untag(word0) / untag(word1) )
         = tag( (word0 / 2) / (word1 / 2) )
         = tag(word0 / word1)
         = 2 * (word0 / word1)
etc.

Obviously these can be derived from basic arithmetic, but it's a bit tedious, so I was wondering if there was a reference describing a full set of such identities, or any more sophisticated optimizations. Perhaps a tag calculus of sorts.

Of course, care must be taken to handle overflow on the word when adding and multiplying, but I think "branch on overflow" is a fairly common instruction, and would provide for an efficient implementation to tweak the result.