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.