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>

lib/riscv refine: move lemma (#33)

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

lib: avoid some syntax warnings

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

lib: cong rules for corres

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

lib: corres rules for abstract-side failure

Treatment of fail/assert/stateAssert when you don't have to prove non-failure
of the concrete side, and lemmas for switching between nf and ¬nf for the
abstract side when no_fail is already proved separately.

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

licenses: convert license tags to SPDX

lib: add corres_cases'

This version augments the schematic preconditions with the knowledge of
which case we are in. It should replace corres_cases eventually.

riscv: cleanup; resolve remaining FIXMEs

global: isabelle update_cartouches

lib: add unit_dc_is_eq

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.