reduce DRefine dependencies from Refine to AInvs

This needs (and includes) some deduplication and moving of lemmas formerly in
refine.

Isabelle2018: Lib update

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

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

lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad

lib: add generic lemmas from SELFOUR-584 updates

Mainly concerning word_ctz and enumeration_both.

lib: Datatype_Schematic and WPFix.

Add two new tactics/methods which can fix common painful problems with
schematic variables.

Method datatype_schem improves unification outcomes, by making judicious use of
selectors like fst/snd/the/hd to bring variables into scope, and also using a
wrapper to avoid singleton constants like True being captured needlessly by
unification.

Method wpfix uses strengthen machinery to instantiate rogue postcondition
schematics to True and to split precondition schematics that are shared across
different sites.

lib: generic/word/monad/hoare lemmas from SELFOUR-242 verification

Notably useful is hoare_vcg_lift_imp' which generates an implication
rather than a disjunction.

Monadic rewrite rules should be modified to preserve bound variable
names, as demonstrated by monadic_rewrite_symb_exec_l'_preserve_names.
Addressing this more comprehensively is left as a TODO item for the
future (see VER-554).

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.

autocorres-crefine: specialise corres_no_failI for compatibility with Refine

The generic rule is now named corres_no_failI_base.

lib: start disentangling spaghetti word dependencies

autocorres-crefine: add pre-no-fail flag to corres. Updated AI+Refine.

fewer warnings

Trace_Attribs: Remove hooks in "Corres_UL" to allow "lib/" to build once more.

attribute tracing: Mechanism to work out changes in simpsets across revisions.

The idea of this file is to allow users to determine how the simpset,
cong set, intro set, wp sets, etc. have changed from an old version of
the repository to a new version.

The process is as follows:

1. A user runs "save_attributes" on an old, working version of the
theory.

2. This tool will write out a ".foo.attrib_trace" file for each
theory processed.

3. The user modifies imports statements as required, possibly
breaking the proof.

4. The user can now run "diff_attributes" to determine what
commands they should run to restore the simpset / congset /etc
to something closer to the old version.

The tool is not complete, in that it won't always suggest the full set
of "simp add", "simp del", etc commands. Nor does it know that a rule
added to the simpset is causing a problem. It merely lists
a hopefully-sensible set of differences.

ported lib/* theories to Isabelle2014-RC0

some of the global Isabelle2014 renames

option_case -> case_option
sum_case -> case_sum
prod_case -> case_prod
Option.set -> set_option
Option.map -> map_option
option_rel -> rel_option
list_all2_def -> list_all2_iff
map.simps -> list.map
tl.simps -> list.sel(2-3)
the.simps -> option.sel

release cleanup

Import release snapshot.