Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM.

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

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

Isabelle2018: new comment syntax

(result of "isabelle update_comments <dirs>")

arm: address setCurrentPD mismatch between abstract/haskell/C

ARM setCurrentPD was recently refactored as part of multi-VM support for
ARM_HYP. The Haskell was updated correctly, and the C was not.
Unfortunately, setCurrentPD was manually redefined in MachineOps.thy for
ARM hiding the change, making the C look correct when it wasn't.

We scrap the second definition of setCurrentPD, load it from the Haskell,
and have an abstract set_current_pd that's a bit simpler to refine down
from.

The proofs are updated for the above change and the update to the C
setCurrentPD that was breaking on KZM.

Proof update for crunch changes

Many proof repairs.

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.

Isabelle2017: update AInvs for RC0

* word_eqI is no longer rule_format.

* Updated Isabelle/ML Thm.join_proofs to Thm.consolidate.

* Updated suffix_refl to suffix_order.order.refl.

* Removed some lines of proofs, thanks to improved simplifier.

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.

SELFOUR-748: rename tlb invalidation functions

ainvs: reintroduce second_level_tables all over the place, update generic Arch_AI and various ArchArch_AI's to match

arm ainvs: Updated up to ArchFinalise_AI

x64: general cleanup, renaming lemmas

backport changes to ARM proofs from X64 work in progress

- replace ARM-specific constants and types with aliases which can be
instantiated separately for each architecture.
- expand lib with lemmas used in X64 proofs.
- simplify some proofs.

Also-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

x64: get ArchVSpace_AI to check

- Fixed some lemmas and their proofs.
- Marked some others as "sorry".
- Removed some lemmas that don't seem relevant to X64.

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-444: AInvs proven for preemptible retype.

x64: more progress in ArchVSpace_AI

SELFOUR-421: fix coding style

arch_split: give some vspace concepts more generic names

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

arch_split: move kernel_base and idle_thread_ptr to arch-specific theories

arch_split: invariants: split InterruptAcc_AI [VER-606]

arch_split: invariants: split Ipc_AI [VER-572]

word_lib: adjust theory dependencies

lib/spec/proof/tools: fix word change fallout

arch_split: fix proofs after removing shadow and unqualify commands and adding fix for crunch. Checks up to DPolicy.

arch_split: replaced sublocale with global_naming

arch_split: invariants: up to Schedule_AI

arch_split: some quick and dirty arch_splitting by selectively interpreting the ARM locale (with FIXMEs)

arch_split: checkpoint. Checks up to ArchVSpace_AI with two sorries (MattB WIP)