lib: A tutorial and some 'modify' monad rules for Lib.EquivValid

Thanks to Toby Murray (@tobycmurray) for early feedback.

Signed-off-by: Robert Sison <robert.sison@unimelb.edu.au>

licenses: convert license tags to SPDX

global: isabelle update_cartouches

lib: tag correctly as BSD

(Two library files were incorrectly tagged as GPL).

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

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

Removes all trailing whitespaces

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

SELFOUR-444: Finished InfoFlow and DRefine.

infoflow: Move "EquivValid" out of "infoflow/", into "lib/".

More importantly, remove seL4 from the dependencies of "EquivValid", so
others can use it.

Also, we fixup the fallout.