Improve [decompose_elem_of] tactic.

Conflicts:
	collections.v
Preparation to port the master branch

Major changes:
* A data structure to collect locked addresses in memory.
* Operations to lock and unlock addresses.
* Remove [ctree_Forall] and express it using [Forall] and [ctree_flatten]. This
  saves a lot of lines of code.
* Add a [void] value. This value cannot be typed, but will be used as a dummy
  return value for functions with return type [void].

Minor changes:
* Various deciders in preparation of the executable semantics.
* Improve naming and notations.
* Remove obsolete stuff.
Port expressions, statements, and smallstep semantics from the master branch.
Preliminary version of an interpreter.