Fix up proofs after word lemma moves

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

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

Proof update for crunch changes

Many proof repairs.

arm ainvs: fix a typo

arm ainvs: wp rules for simple_ko setter/getter

arm : add AEndpoint and ANTFN a_type simplification

in addition to the a_type ATCB simplification, the following two are now in the simpset:
"a_type (Endpoint x) = AEndpoint"
"a_type (Notification v) = ANTFN"

arm: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242)

Colloquially known as "invert-fastpath".

Update verification efforts on ARM for the following seL4 changes:
- scheduling decisions done in possibleSwitchTo are moved to the
scheduler
- possibleSwitchTo only checks whether the candidate is valid for a
fast switch, not its priority, accepting possible candidates
immmediately as a switch-to scheduler action
- the scheduler checks the candidate against the current thread and
against the bitmaps before making a decision
- attemptSwitchTo and switchIfRequiredTo are gone
- scheduler is now more complicated, and numerous proofs related to it
are rewritten from scratch
- fast path now checks ready queues via the scheduler bitmaps
- L2 scheduler bitmap order reversed for better cache locality

Many iterations between the kernel and verification teams were needed
to get this right.

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.

Removes all trailing whitespaces

arm ainvs: Update for create_mapping_entries changes

arm ainvs: update arch stuff to match generic for top level ainvs files

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

AInvs: genericise Detype_AI.thy

update references to word32_plus_mono_right_split

This is now called machine_word_plus_mono_right_split, since it now
works at the current architecture's machine word size.

SELFOUR-553: update rpidrurw in TCBConfigure for simpler Infoflow proofs.

SELFOUR-553: Change Spec according to C code and fix ASpec and AInvs

SELFOUR-64: Remove general Recycle operation

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

SELFOUR-444: Haskell implementation, begin refine.

First attempt at a haskell implementation of preemptible retyping
and the refinement proof to abstract.

SELFOUR-444: AInvs proven for preemptible retype.

SELFOUR-421: fix coding style

arch_split: split PDPTEntries_AI, rename as VSpaceEntries_AI [VER-580]