Add delete_delete thm to sptreeTheory

Cleanup of append thms for SORTED

Remove redundant compute annotation

Move [compute] annotation for subspt to right place

Replace unicode in previous

Improve sptree toSortedAList

Adding run-length-encoding to toSortedAList solves the problem with
sparse trees, so toSortedAList is now respectably fast to EVAL in
all cases. This version is slightly slower than the previous for
packed trees, but it doesn't seem worth trying to fix that.

Make num_map and num_set printing type abbreviations for sptrees

Provide print-only syntax for ground sptree values

E.g.,

> ``BN (LS v) (LS w)``;
<<HOL message: inventing new type variable names: 'a>>
val it = “⦕ 1 ↦ w; 2 ↦ v ⦖”: term

There's a trace to turn it off. Considering enabling it as input
syntax as well.

Remove older of Theorem syntaxes (the one with the quotes)

It's confusing to allow two, and it seems pretty clear that the
Proof-QED proof is nicer.

Deal with bad rebindings of theorems under src/

In bag, a name was reused for a different theorem so a name change was
required. Elsewhere, the same theorem was stated and proved more than
once so redundant stuff could be deleted.

Import a number of sptree theorems from CakeML

Most about the subspt relation

Remove copied unicode.

Update for Theorem= syntax.

Add toSortedAList to sptree.

Adds an O(n) traversal of sptree's that extracts an
association list sorted in index order. The absence
of such a traversal was noted as a major drawback
in the existing documentation.

The algorithm is adapted from the one for Braun trees
(sptree's are Braun trees with gaps/partiality added).
It won't handle very sparse arrays well, that is, it's
O(n) in the largest index, not the number of elements.

Start merging finite_map/dictionary theories into one directory

Aim is to also include src/enumfset, possibly also the balanced_bst
development from examples, and a CakeML theory (alist_tree).

With all this stuff in the same place, we reduce branching under src/
and get better concurrency when building.