all: remove theory import path references

In Isabelle2020, when isabelle jedit is started without a session
context, e.g. `isabelle jedit -l ASpec`, theory imports with path
references cause the isabelle process to hang.

Since sessions now declare directories, Isabelle can find those files
without path reference and we therefore remove all such path references
from import statements. With this, `jedit` and `build` should work with
and without explicit session context as before.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX

lib: Add stray lemmas and methods.

These were unused items in ARM CRefine, now kept for potential future
usefulness.

Isabelle2018: Lib update

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

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

lib: add generic lemmas from SELFOUR-584 updates

Mainly concerning word_ctz and enumeration_both.

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.

Isabelle2016-1: update references to renamed constants and facts

Lib: Addition of auxiliary lemmas in basic theories to better support CRefine

* Generalized version of bind_inv_inv_comm for easier swapping inside
the nondet monad

* New ccorres_symb_exec_r_known_rv

* New zip_take lemmas for handling `take n (zip x y)` situations

tags: [VER-623][SELFOUR-413]

lib/spec/proof/tools: fix word change fallout

more fixes in DRefine: some changes in proofs involving uint / unat

autocorres-crefine: update CRefine with new corres_UL.

Finally done with array assertions.

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.