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

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

arm: ioportcontrol: Fixes after adding IOPortControlCaps to x64

Proof update for crunch changes

Initial proof updates for combinator changes.

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.

Remove valid_arch_objs

now that we have valid_vspace_objs to express validiy of
vspace objects, we do not need valid_arch_objs: we have
valid_objs to state the validity of non-vspace arch objects.

Removes all trailing whitespaces

arm ainvs: updated proofs in ArchBCorres2 + KernelInit + ArchInterrupt

arch_split x64 arm: make cte_level_bits an arch constant

ainvs: repair wp_pre fallout

update invariants for prepare_thread_delete

wp_cleanup: update proofs for new wp behaviour

The things that usually go wrong:
- wp fall through: add +, e.g.
apply (wp select_wp) -> apply (wp select_wp)+

- precondition: you can remove most hoare_pre, but wpc still needs it, and
sometimes the wp instance relies on being able to fit a rule to the
current non-schematic precondition. In that case, use "including no_pre"
to switch off the automatic hoare_pre application.

- very rarely there is a schematic postcondition that interferes with the
new trivial cleanup rules, because the rest of the script assumes some
specific state afterwards (shouldn't happen in a reasonable proof, but
not all proofs are reasonable..). In that case, (wp_once ...)+ should
emulate the old behaviour precisely.

Isabelle2016-1: rename free variables to avoid capture

Isabelle2016-1: update references to renamed constants and facts

SELFOUR-64: Remove general Recycle operation

This removes the RecycleCap CNodeInvocation, whilst
retaining recycle behaviour for Endpoints -- now renamed
CNodeCancelBadgedSends.

SELFOUR-421: fix coding style

Refactor of crunch.

Substantial adjustments to crunch. Main user changes are:
- 'lift' and 'unfold' mechanisms replaced by more general 'rule'.
- some more 'ignores' standardised.
- crunch has a more principled overall design:
+ discover crunch rule
* provided or by definition extraction
+ recurse according to rule
+ prove goal based on rule, recursive discoveries, standard tactic
* wp/simp adjustments tweak tactic

arch_split: give some vspace concepts more generic names

In particular rename "pd" to "vspace", when the pd represents
an address space.

arch_split: invariants: split CNodeInv_AI [VER-573]

arch_split: skeleton arch files for AInvs