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

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

arm: ioportcontrol: Fixes after adding IOPortControlCaps to x64

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.

ainvs: integrate all architectures

Removes all trailing whitespaces

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

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: fix ArchRetype_AI

- Port from ARM to X64:
- Definitions and lemmas relating to copy_global_mappings.
- Device untyped patch.
- Pre-emptible retype patch.

Includes some fixes to ArchVSpace_AI and ArchVSpaceAcc_A.

There is one "sorry" in ArchRetype_AI which is waiting for a refactoring
of ArchAcc_AI and ArchVSpace_AI for simpler proofs concerning vs_lookup,
store_pml4e, etc.

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: update references to renamed constants and facts

AInvs: remove 32-bit references in Untyped_AI

SELFOUR-444: AInvs proven for preemptible retype.

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: invariants: tidied

arch_split: invariants: split Retype_AI [VER-556]

arch_split: access: fixup locale introduction rule

arch_split: skeleton arch files for AInvs