Fix up proofs after word lemma moves

Remove pure word lemmas from proof/*

Removes redundant lemmas after moving them up to Word_Lib.

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

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

crefine: further update for C-parser change to avoid complex call lvals (JIRA VER-881)

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

Apply "invert-fastpath" changes to arm-hyp (ainvs, refine, crefine).
See main commit for arm for more context.

update object and field widths for x64, and remove some magic numbers

In X64 update the following to match the C kernel:
- TCB size-bits (11).
- Endpoint size-bits (4).
- Guard bits (58).
- Message registers.

For all architectures, replace magic numbers with defined constants in
specifications, and as far as possible in proofs:
- tcb_bits in abstract spec.
- tcbBlockSizeBits, cteSizeBits, ntfnSizeBits, epSizeBits in Haskell
spec, Haskell and C refinement proofs.

arm-hyp crefine: bitfield generator proof updates

SELFOUR-748: rename tlb invalidation functions

arm-hyp crefine: Recycle_C sorry-free

arm-hyp crefine: sorry Finalise_C Recycle_C Arch_C

Fixed the easy lemmas, but Arch_C has lots of issues outstanding.

arm-hyp crefine: update ARM*. with ARM_HYP*. qualification

Found three quantification flavours styles: ARM. ARM_A. ARM_H.

Via find|sed on entire folder.

arm-hyp crefine: copy from ARM