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: avoid ambiguous syntax

lib: more lifting rules for validE_R and validE_E

lib: wp cleanup and parser improvements

The main visible change is from wp_trace', 'wp_once' and 'wp_once_trace' to
'wp (trace)', 'wp (once)' and 'wp (once, trace)'. The option for printing a
warning for unused supplied wp rules has also been removed.

lib: three lemmas moved from refine theories

lib: move up library lemmas from RISCV64 and X64

global: isabelle update_cartouches

ainvs: update for new definition of set_object

Added set_object_wp_strong, which infers from a given hoare triple with
command set_object that the object of same type already exists in the
heap, and hoare_set_object_weaken_pre which does the same thing, but can
be applied on top of existing lemmas about set_object.

ainvs: improve proof of set_thread_state_runnable_valid_blocked

ainvs: change return value to a more general one

in_set_object has a return value that is empty '()', but the theorem
still holds true when replaced with a generic parameter 'rv' making it
easier to use this lemma.

ainvs: trivial - updated style of proof

ainvs: strengthen set_object_idle lemma

Add conditions imposed by valid_idle into precondition.
Thank you to Matt Brecknell for the help.

ainvs: abbreviated Hoare triples and proof fix

ainvs: restated set_object_wp_strong with auxiliary lemmas

ainvs: update for new definition of set_object

ainvs: update for new definition of set_object

Move in a few set_object and set_aobject theorems from x64 theory files
as these theorems were architecture generic.

ainvs: update for new definition of set_object

ainvs: update for new definition of set_object

lib: add a comb parameter to wpsimp, along with two new comb rules

Base ASpec + machine on OptionMonad_ND; fix proof fallout

lib: option (reader) monad syntax and gets_map operator

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

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

lib: add non-cond-simplification, use in wpsimp.

Adds "non-conditional simplification" method simp_no_cond, and
various equivalents.

This is done by setting the simplifier depth limit to 0, which seems
to be a useful case. It prevents expensive conditional simplification
attempts but leaves the simplifier strategy otherwise unchanged.

This is easy to set up, and link to wpsimp.

lib: fundef termination rule for unlessE .. $ throwError ,,

lib: add generic lemmas from SELFOUR-584 updates

Mainly concerning word_ctz and enumeration_both.

lib/wp: Adjust some problematic attributes.

In particular, some intro! attributes for some wp rules are removed.
These previously caused auto/fastforce to play a really strange role
in some proofs.

lib/wp: Standard when/unless/whenE/unlessE rules.

The rules for these conditional monadic operators have been a bit
ad-hoc until now, with frequent headaches around the whenE/throwError
pattern.

Adding standard split rules ensures these operators are treated uniformly.

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/wp: Bundle to restore classic combinators.

The previous combinator change is desirable, but some proofs are too
difficult to fix. This bundle restores the classic behaviour.

lib/wp: Remove old wp combinator rules.

These combinator rules do something like what wp_pre does now.

They were helpful in the ancient past, but now that wp_pre exists it is
much better to just use automation.

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).

lib: more modifiers for wpsimp (wp_del, simp_del)

Removes all trailing whitespaces

changes after rebasing (for isabelle2016-1 and the new wp)

arm-hyp invariants: Changes to non_vspace_obj and valid_vso_at

tags: [VER-670]

lib/wpsimp: pass more parameters to clarsimp

lib: faster proof

wp: wpsimp and bundle no_pre

- small wpsimp method that wraps up the standard (wp|wpc|clarsimp)+ pattern
- a bundle "no_pre" that removes the wp_pre rules for situations where the
old wp behaviour is wanted.

Isabelle2016-1: update references to renamed constants and facts

lib: start disentangling spaghetti word dependencies