Isabelle2018: Lib update

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

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

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.

Removes all trailing whitespaces

lib: Adding some lemmas about init

* init_Snoc: init (xs @ [x]) = xs

* init_upto_enum_upt: init [0.e.n] = [0..<n]

wp_cleanup: update proofs for new wp behaviour

The things that usually go wrong:
- wp fall through: add +, e.g.
apply (wp select_wp) -> apply (wp select_wp)+

- precondition: you can remove most hoare_pre, but wpc still needs it, and
sometimes the wp instance relies on being able to fit a rule to the
current non-schematic precondition. In that case, use "including no_pre"
to switch off the automatic hoare_pre application.

- very rarely there is a schematic postcondition that interferes with the
new trivial cleanup rules, because the rest of the script assumes some
specific state afterwards (shouldn't happen in a reasonable proof, but
not all proofs are reasonable..). In that case, (wp_once ...)+ should
emulate the old behaviour precisely.

Isabelle2016-1: update references to renamed constants and facts

word_lib: adjust theory dependencies

fewer warnings

lib: Remove malformed comment.

This comment looks like a typo, in that it doesn't add to comprehension of this
theory, and it trips up LaTeX when generating a document.

ported lib/* theories to Isabelle2014-RC0

Import release snapshot.