Significant step towards a fully functional tree-based refinement

Rewrote the entire tree-based example to use the new nested trees
framework. Observers are fully refined and proved, while some parts of
the mutators are still admitted.

In the process, the dual list/tree structure that the example was
previously using was unified into a single nested tree structure, and
the State inductive types was replaced with nats (though it could
possibly use bounded strings in the future). As a consequence, the list-
based example was removed from the Makefile.
Merge branch 'master' of /afs/csail.mit.edu/group/plv/git/adt-synthesis
Get rid of the unitialized existentials

The leftover existentials were due to a glitch in the typeclass
resolution; specifying the bag instance by hand solves it.
Fully refined tree-based process scheduler example

Get rid of the three pending admits using the binsert_enumerate
predicate, and the insert_always_happens lemmas. Bottom line: it works!

The tree-based refinement is now in the Makefile, and the Bookstore
example has been moved to the end as it had the highest compile times.
Moved library and examples into different directories.
Moved QueryStructure code around.
Merge branch 'master' of file://///afs/csail.mit.edu/group/plv/git/adt-synthesis

Conflicts:
	Makefile
More merging.
Move file moving.
Moved QueryStructure Examples
Preliminary work on caching

Introduce a caching-able bag interface. Forseeable difficulties include:
* Our set-based specifications of queries only describe results in terms
of membership, thus allowing duplication in the computed result set. For
this reason, cacheable functions are restricted to morphisms of the
SetEq predicate (ie. the cached function f must verify (forall x, In x
seq1 <-> In x seq2) -> fold f seq1 = fold f seq2. max is an example of
such a function, but other functions such as sum are not. Adding non-
duplication to the specification or to the Bag interface will make
implementation of some indexing systems harder. On the other hand, there
is a case for disallowing spurious repetitions.
* The equivalence relation between aggregated results in the caching
interface is equality, while clients might want to keep traces of things
like 'top n elements', which would require a different equivalence
relation (in this example, Permutation).
Make it easier to cache the result of a projection
Add typing information to ForAll_In

The type inference process chose (@Tuple BoundedString), but the
arguments passed to this function are only database rows, so the
BoundedString can be made more explicit.
Full tree-based refinement using the caching interface

Two areas remain ungraceful:
* The handling of caching specifications over projections of items vs.
simple values is ugly.
* An assert in required in the refinement of SPAWN.
Minor code cleanups in the tree-based example

The 'Defined' call still takes insanely too long
Start cleaning up Bags.v
Hide the proofs in the IndexedBagAsBag typeclass implementation

Proving the various lemmas separately solves the performance problem
observed when calling Defined in TreeBasedRefinement.v.
Large cleanup of the Bags and ProcessScheduler codebases
Qed all the typeclass instance proofs in CachingBags

The performance improvement in TreeBasedRefinement.v is less obvious
than in the previous commit. Also, using section variables would
probably make everything a lot cleaner in CachingBags.
Further cleanup the TreeBasedRefinement example

The next logical step would probably be to devise an automated way of
deriving the insert_always_happens lemmas.