licenses: convert license tags to SPDX

word_lib: shorter, more automatic proofs

lib, x64 crefine: remove word lemma unat_ucast_8_64

unat_ucast_8_64 states that upcasting an 8 word to a 64 word does not
changes its value. We have a generic lemma for this which can be
specialised to this lemma: unat_ucast_up_simp[where 'a=8 and 'b=64,
simplified].

lib/Word_Lib: sync with AFP

Isabelle2018 lib: Word_Lib

lib: add some word lemmas about sless, word_bits

Removes all trailing whitespaces

backport changes to ARM proofs from X64 work in progress

- replace ARM-specific constants and types with aliases which can be
instantiated separately for each architecture.
- expand lib with lemmas used in X64 proofs.
- simplify some proofs.

Also-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

Isabelle2016-1: update Word_Lib

Word_Lib now looks more like the current AFP entry, though there are
still some local modifications.

Word_Lib: Add Suc_unat_mask_div to Word_Lemmas_64

Word_Lib: lemmas comparing different word sizes

lib: fixed 64 bit includes

Word_Lib: added 64-bit word instances

Word_Lib: added 64-bit word instances