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>")

access-control, infoflow: use generic relation for pasDomainAbs

This patch generalises the mapping between authority labels and
scheduler domains, so that the access-control integrity property still
holds when labels are not partitioned into domains. This lets us use
the integrity result on systems that don't use the domain scheduler.

The information flow proofs still rely on the domain partitioning,
hence we add constraints on the label-domain mapping for the info-flow
results to hold.

Jira VER-945

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.

Removes all trailing whitespaces

Isabelle2016-1: update references to renamed constants and facts

Updating remaining proofs for tcb_arch reserved_irq and arch_fault changes

* tcb_context rephrasing to (tcb_context o tcb_arch) and respectively
for set operations

* unfolding of reserved_irq for trivially solving most lemmas

* Changes to the inductive definition of integrity_obj to account for
tcb_arch and tcb_context new location

* Changes to the tcb examples in ExampleSystem to include tcb_arch

* Rephrasing of domain_sep_inv to accommodate the ReservedIRQ case

* Mostly rephrasing of tcb_context to (some form of) (tcb_context o tcb_arch)

* Trivial unfolding of handle_reserved_irq for hoare rules

* Examples in Example_Valid_State.thy were updated

* Nothing remarkable, mostly rephrasing of tcb_context and ReservedIRQ
handling

* Fun fact, some proofs are now shorter

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

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

SELFOUR-444: Finished InfoFlow and DRefine.

SELFOUR-444: Logic generalised; Access finished.

Tweak AInvs proof for Untyped to be more reusable, finish integrity
proofs.

SELFOUR-421: fix coding style

SELFOUR-421: infoflow and infoflow_c builds

SELFOUR-421: crefine builds

arch_split: requalify abstract theories

arch_split: Access checking

SELFOUR-56: Remove diminish rights from IPC

l4v-sabre: change type of irq to be 10 word

arch_split: Access and InfoFlow now build

add arch_tcb object to C, rename aep -> ntfn

history squashed patch for aep-binding

Access: Fix trivial comment typo.

2015 update for access

Fix Access, InfoFlow and DRefine.

Proof updates, working as far as AInvs.

some of the global Isabelle2014 renames

option_case -> case_option
sum_case -> case_sum
prod_case -> case_prod
Option.set -> set_option
Option.map -> map_option
option_rel -> rel_option
list_all2_def -> list_all2_iff
map.simps -> list.map
tl.simps -> list.sel(2-3)
the.simps -> option.sel

Import release snapshot.