drefine: Isabelle2020 update

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX

global: isabelle update_cartouches

reduce DRefine dependencies from Refine to AInvs

This needs (and includes) some deduplication and moving of lemmas formerly in
refine.

Isabelle2018: DRefine

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

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

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]

arch_split: fix proofs after removing shadow and unqualify commands and adding fix for crunch. Checks up to DPolicy.

arch_split: DRefine checking

more fixes in DRefine: some changes in proofs involving uint / unat

arch_split: DRefine now builds

add arch_tcb object to C, rename aep -> ntfn

history squashed patch for aep-binding

2015 update for DRefine

Fix Access, InfoFlow and DRefine.

Refine working.

option_map_def -> map_option_case for 2014-RC0

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

release cleanup

Import release snapshot.