Allow memory refinements to behave like simple renaming.

Memory refinements now carry a boolean parameter that has the following
meaning:

[false] : Behave like a simple renaming of memories that merely allows to
          permute object identifiers. It does not allow to refine memories
          into a more defined version.
[true]  : Behave like before. Objects can be injected, and memory contents can
          be refined into a more defined variant.

We make refinements parametric in these two variant to avoid code duplication,
and because the [false] variant is a special case of the [true] variant.

For completeness of the executable semantics, we now use the [false] variant.
Swap arguments of meminj_compose, they were in the wrong order.
Move refinement stuff to separate files to speed up compilation.
Stronger completeness proof for the executable semantics.

The proof now uses the stronger notion of memory permutation instead of a more
general memory refinement. We have also proven that memory permutations are
symmetric.