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.

Removes all trailing whitespaces

SELFOUR-748: rename tlb invalidation functions

arm ainvs: added necessary locale assumptions in ArchIpc_AI

arm ainvs: Updated up to ArchFinalise_AI

Isabelle2016-1: update references to renamed constants and facts

AInvs: Updating arch-specific theories for tcb_arch reserved_irq and arch_fault

* Rephrasing of all the lemmas that used to refer to tcb_context as
a direct value on tcb.

* Providing arch-specific lemmas about handle_arch_fault_reply and
make_arch_fault_msg to deal with handle_fault_reply and make_fault_msg
new arch-specific cases.

* Trivial but arch-specific proofs about reserved_irq

tags: [VER-623][SELFOUR-413]

SELFOUR-421: fix coding style

arch_split invariants: TcbAcc_AI

Somehow we missed this on our previous pass.

arch_split: invariants: split CSpaceInv_AI [VER-604], CSpace_AI [VER-605]

arch_split: replaced sublocale with global_naming

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)