Fix computability thy's in light of pat_assum rename

Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

Improved version of the 'Ackermann not p.r.' proof.

Nicer because it no longer has to use MAX, among other things.

Export 'strong' primrec indn; and move num-list theorems back to prnlistTheory.

Moved Pr1 constant from prterm to primrecfns, allowing some simpler proofs.

Show that "is an abstraction" and "is in beta-normal form" are prim rec.

In both case, these are computable functions over numbers encoding de
Bruijn terms.

Recast tri, invtri, npair, nfst and nsnd to use pr1 and pr2 lifiting functions.

Use pr1 and pr2 "lifting" functions to remove need for some constants.

For example, pr_add is now (pr2 $+), and pr_mult is (pr2 $*). Haven't
quite finished this process (want to do the numeric pairing functions
similarly).

Start of an effort to lessen the need for explicit prim. rec definitions.

Instead, the theory is that I will show theorems like

|- primrec (pr2 $+) 2
|- primrec (pr2 $*) 2
|- primrec (pr2 $DIV) 2

and then I'll be able to use (pr2 $+) everywhere instead of pr_add,
saving on excess constants. Of course, to show the primrec theorems,
I will have to express the given functions using the primitive
recursive building blocks.

Prove that numeric pairing (via calculation of triangular numbers) is prim rec.

Prim. rec. functions now do something reasonable with lists of wrong size

Recast theory to have the primitive recursive functions act on lists
of numbers, rather than single numbers encoding lists of numbers.

Prove that div and mod are primitive recursive.

Add a comment attributing my Ackermann Proof (to Gregory Taylor).

Complete proof that Ackermann's function grows faster than any
primitive recursive function.

Start of a theory of primitive recursive functions.
Almost finished proof that Ackermann's function is not prim. rec.