licenses: convert license tags to SPDX

global: isabelle update_cartouches

lib: Change Add_Locale_Code_Defs to filter out rules with sort hypotheses.

Expand eval_bool; add a method word_eqI_solve.

A number of proofs begin with word_eqI followed by some similar steps,
suggesting a 'word_eqI_solve' proof method, which is implemented here.

Many of these steps are standard, however a tricky part is that constants of
type 'nat' which encode a particular number of bits must often be unfolded.
This was done by expanding the eval_bool machinery to add eval_int_nat, which
tries to evaluate ints and nats.

Testing eval_int_nat revealed the need to improve the code generator setup
somewhat. The Arch locale contains many of the relevant constants, and they are
given global names via requalify_const, but the code generator doesn't know
about them. Some tweaks make them available. I *think* this is safe for
arch_split, as long as the proofs that derive from them are true in each
architecture.

Add some methods to trym.

New eval_bool method, evaluated boolean terms.

This method/simproc uses the code generator setup to evaluate terms of boolean
type that can be reduced to True/False. Should avoid manual unfolding in
various places.