licenses: convert license tags to SPDX

riscv: cleanup; resolve remaining FIXMEs

lib: move more facts on Numeral_Type from invariant proofs into lib

lib: move up library lemmas from RISCV64 and X64

lib: complete/full induction for Numeral_Type

lib: additional library lemmas for Numeral_Type

global: isabelle update_cartouches

lib: additional setup for numeral types

In particular: instantiate to the size class so one can use bounded types
for automatic termination measures in fun.