Investigate greater use of heap projections in Invariants_H.thy

[michaelmcinerney]

Greater use of heap projections in invariants and in state_relation may ease some reasoning in Refine.

For example, pspace_relation, the greatest component of state_relation, could make far greater use of heap projections, in a way similar to what is done in cstate_relation in CRefine. For example, we could write pspace_relation as a conjunction over the various kernel object types, each saying, for example, that given an abstract heap of TCBs (with tcbs_of) and a concrete heap of TCBs (with tcbs_of'), that their domains are equal, and that at the points in the domain, tcb_relation holds between the abstract and concrete TCBs.