Fix p/printing in untested (& unused?) patriciaLib

Further clean-up patriciaLib code.

Update to patriciaLib code.

Following these updates, most conversions are now faster.

** Note that PTREE_TRANSFORM_CONV, PTREE_EVERY_LEAF_CONV and PTREE_EXISTS_LEAF_CONV now take a conversion as an extra argument.

** The reference is_ptree_term_size_limit has been removed.

Instead, there are now two functions: Define_mk_ptree and Define_mk_ptree_with_is_ptree. The latter returns an IS_PTREE theorem for the new constant. In this case the IS_PTREE theorem is proven in a more efficient manner, however it can still be time consuming, e.g. on a fast machine it takes 3 minutes to prove for a tree with around 49 thousand elements. Smaller trees are more manageable, e.g. 1.6s for a tree with a thousand elements.

Patch up patricia_castsLib.

Minor tweaks.

Remove some theorems that Thomas added to listTheory.

Also added TRAVERSE_AUX which is now used to evaluate TRAVERSE and KEYS.

A Patricia tree implementation of finite maps, with datatypes ``: 'a pree``
and ``: ('a, 'b) word_ptree``. These provide support for finite maps

num |-> 'a
'a word |-> 'b
string |-> 'a

For example:

- load "patriciaLib";
- EVAL ``(Empty |+ (1, 1) |+ (2,2)) ' 1``;
> val it = |- (<{}> |+ (1,1) |+ (2,2)) ' 1 = SOME 1 : thm

There is also support for representing sets i.e. num set, 'a word set
and string set.

For example:

- load "patricia_castsLib";
- EVAL ``32w:word32 IN_PTREEw +{16w; 12w; 32w; 8w}+``;
> val it = |- 32w IN_PTREEw +{16w; 12w; 32w; 8w}+ = T : thm
- EVAL ``KEYSs -{"world"; "hello"}-``;
> val it = |- KEYSs -{"world"; "hello"}- = ["hello"; "world"] : thm
- EVAL ``NUMSET_OF_PTREE <{2; 4; 6; 2}>``;
> val it = |- NUMSET_OF_PTREE <{2; 4; 6; 2}> = {6; 2; 4} : thm

It is also possible to work with large trees by constructing them in ML.

For example:

- val tree = patriciaLib.ptree_of_ints (2::l); /* very long list of ints */
- Globals.max_print_depth := 10; /* tree is too big to print in full */
- val tree_def = patriciaLib.Define_mk_ptree "tree" tree;
- EVAL ``2 IN_PTREE tree``;
> val it = |- 2 IN_PTREE tree = T : thm
- EVAL ``tree \\ 2``;
> val it = |- tree \\ 2 = tree \\ 2 : thm
- EVAL ``2 IN_PTREE (tree \\ 2)``;
> val it = |- 2 IN_PTREE tree \\ 2 = F : thm

All of this happens fairly quickly, even when there are a few thousand
elements in the tree -- that is, when adding tree_def to the compset
would make things grind to a halt.