Initial version new memory.
Improve "decompose_Forall_hyps" tactic.
Improve "choosing an element" of a finite collection.
Improvements of new memory.

* Make types more C-ish, by disallowing arrays, structs and unions of size 0.
* Remove sizes for arrays values.
* Only require the size of base types to be positive, we can prove it for
  other types.
* Nicer notations for C-types.
* Start on implementing unary/binary operations and casts.
More uniform notation for valid pointers/bytes.
Avoid generation of some induction schemes.
Some clean up in list.
Define ⊑@{m} on memory values using "mval_of_bytes" instead of "mval_of_bytes".

This makes it more consistent with values.
Change the definition of "is_Some" to use an existential.
Add "as ident(H)" to the "case_bool_decide" tactic.
Misc updates to the prelude.
Type classes for finite and countable types.
Update of new memory model.

Most important changes:
* Indeterminacy and pointer fragments on the level of bits, instead of bytes.
* More simple axiomatization of integers, now we use plain [Z]s together with
  predicates to capture overflow etc.
* Remove non-deterministic encoding of values as memory values.
* Construction of the actual memory
Remove operational and axiomatic semantics from this branch.
Add [reshape] function on lists.
Misc prelude changes.
Prove correctness of a version of memcpy external to the memory.
Improve comments, some renaming.
Finite maps and sets using ordered association lists.

This commit includes the following changes:
* More theorems about pre-, partial and total orders.
* Define the lexicographic order on various commonly used data types.
* Mergesort and its correctness proof.
* Implement finite maps and sets using ordered association lists.
More efficient conversion of pmap to association lists.