Fixed to build balanced_bst given changes in 93036c73b4

Achieve this by making comparisonTheory a bit more backwards
compatible. Changes to balanced_bstScript.sml are just to add a bunch
of

val _ = print "Proved lemma\n";

messages after Q.prove calls. This makes it
easier to see that the script is making progress as it executes.

Add some theorems about toAscList

Add lookup_insert theorem to balanced_map

Fix examples/balanced_bst for new by

Fix proof broken by 9a822fc3 (DROP/TAKE change)

Fix balanced_bst theory given changes from 1f63d5f

Fix balanced_map theory to build with new lc simp

Move comparisonTheory to src/enumfset

(from examples/balanced_bst)

Prove a theorem relating most of the definitions in comparisonTheory to
something in totoTheory.

Also, add a new definition for inverting cpns.

Make the overloads on the constructors of cpn permanent in
comparisonTheory.

Turn on totoTheory's "BigSig" to get more useful exports.

This is work towards integration, but the approach has been towards
plurality, i.e. keeping multiple definitions around and proving
relationships between them. More integration could be possible. Also,
the dependency between toto and comparison could be flipped (I wanted to
write new proofs in the nicer environment of comparison so did not do
that.) It has become apparent that totoTheory is in various minor ways
not self-consistent (esp. with regard to its naming schemes).

delete trailing whitespace in examples/balanced_bst

reuse cpn datatype from totoTheory in comparisonTheory

rather than creating an isomorphic new type.

balanced_mapScript.sml has apparently (but not actually) significant
changes because the proofs depend heavily on the order in which the
comparison datatype constructors are defined (inasmuch as it affects the
order of subgoals from cases/induction).

Add a verified balanced binary tree example

This is based on the implementation of weight balanced binary search
trees in the ghc Haskell compiler's standard library.

comparisonScript.sml has a basic theory of comparisons that return
either Less, Greater, or Equal. This is not compatible with the existing
totoScript.sml, because I don't require cmp x y = Equal ==> x = y, but
it does.

osetScript.sml uses the balanced trees to implement sets.

Functional correctenss of the operations is verified, along with the
balancing properties.