Isabelle2018: new "op x" syntax; now is "(x)"

(result of "isabelle update_op -m <dir>")

Genericise deletion actions that occur after empty_slot

This patch adds a generic "post_cap_deletion" step that is called by
finalise_slot. Previous to this, the only caps which had actions
required at this stage were IRQHandlerCaps -- it was required that the
IRQ bitmap be updated after the cap itself was removed (as the
invariants state that for any existing IRQHandlerCap, the corresponding
bit in the IRQ bitmap must be set).

By genericising this, we add the capacity for new, arch-specific post
cap deletion actions to occur in the future.

arm-hyp invariants: new liveness definition

* the definition of liveness is extended for tcb/vcpu reference
* proved liveness related properties for dissociate_vcpu_tcb, prepare_thread_delete, etc.

changes after rebasing (for isabelle2016-1 and the new wp)

arm-hyp invariants: fix arch_splitting/locales

* tcb_arch_ref: definition and invariants (to access obj_refs in tcb_arch in generic contexts)
* fixes related hyp_refs

arm-hyp invariants: changes from rebase for ARM_HYP invariants

arm-hyp invariants: updates for vcpu, alignments, valid_vspace_obj, wellformed_arch_obj, etc.

arm-hyp invariants: copy arch-splitted invariant files from ARM

earlier updates in ArchInvariants are kept