licenses: convert license tags to SPDX

lib: rename lemma to prevent collision with List.sorted_filter

lib: add two lemmas about the sorted predicate

Courtesy of @jalim.

lib: move FastMap lemma to LemmaBucket

Word_Lib: consolidate LemmaBucket and Lib lemmas into Word_Lib

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: add foldl lemma to LemmaBucket

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

Removes all trailing whitespaces

lib: word and misc lemmas from SELFOUR-242 proofs

These precipitated out during cleanup.

backport changes to ARM proofs from X64 work in progress

- replace ARM-specific constants and types with aliases which can be
instantiated separately for each architecture.
- expand lib with lemmas used in X64 proofs.
- simplify some proofs.

Also-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

Isabelle2016-1: update references to renamed constants and facts

lib: move generic lemmas from AInvs to lib

Revert SELFOUR-242: invert bitfield scheduler and optimise fast path

This reverts:
- a67b443ca5a1e4a8f4d4a7fe0757861e2a7898b5
"SELFOUR-242: update goal number based indentation in Fastpath_C"
- f704cf04044209df996ef6c22bc8ea52122a2c1e
"SELFOUR-242: invert bitfield scheduler and optimise fast path"

Verification confirmed functional correctness and refinement of the
system in this case. However, guarantees on thread scheduling and
fairness are not modeled in the current verification. Once this issue is
addressed, SELFOUR-242 will be re-examined.

SELFOUR-242: invert bitfield scheduler and optimise fast path

* Reverse the level 2 of the bitmap scheduler to move the highest priority
threads' level 2 entries into the same cache line as the level 1.
* Use the bitfield scheduler to make the fast path a more common occurrence.
* Change possibleSwitchTo to not invoke scheduler when the fast path would not
invoke it either (using implicit assumptions about the current thread being
the highest priority schedulable thread)

lib: start disentangling spaghetti word dependencies

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

removed deleted theories from imports

Move strengthen rules to Strengthen; adjust WPBang.

lib: Another CAmkES helper lemma.

lib: More random helpers brought to you by CAmkES.

lib: Some pair-related lemmas for LemmaBucket.

lib: Some pair-related lemmas for LemmaBucket.

lib: Some more trivial map-related lemmas.

lib: More trivial helpers from CAmkES.

lib: Fix: Rename duplicate lemma.

...and now back to our regularly scheduled program.

lib: Another trivial lemma for supporting CAmkES.

lib: Import various helper lemmas from CAmkES.

lib: Add a trivial lemma about `dom`.

This comes in handy when reasoning about large maps.

lib: Various trivialities related to CAmkES/CapDL proofs.

This commit contains a grab bag of lemmas used in CAmkES↔CapDL correspondence
proofs. Some of them are exceedingly brain dead. This is, in most cases,
because they have been extracted from automated proofs in order to avoid
generated proofs repeatedly proving the same trivial facts.

lib: Misc helper lemmas.

lib: misc lemmas.

lib: trivial helper for dealing with ∀ and pairs.

Comes in handy when juggling validNF_make_schematic_post in combination with a
Hoare triple with multiple bound variables.

lib: yet more helper lemmas.

Import release snapshot.