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: add lemmas from RISCV64 theories

Some improved ccorres lemmas, dealing with throw and catch, and usual
assortment of misc list/set/map lemmas.

Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>

licenses: convert license tags to SPDX

lib: add lemma hoare_vcg_disj_lift_R

Lifts a Hoare triple with disjunctions in the pre and post-conditions
into two separate Hoare triples.

lib: three lemmas moved from refine theories

lib: update for Isabelle 2019

lib: remove obsolete theory import

lib: option (reader) monad syntax and gets_map operator

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

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

globally use session-qualified imports; add Lib session

Session-qualified imports will be required for Isabelle2018 and help clarify
the structure of sessions in the build tree.

This commit mainly adds a new set of sessions for lib/, including a Lib
session that includes most theories in lib/ and a few separate sessions for
parts that have dependencies beyond CParser or are separate AFP sessions.
The group "lib" collects all lib/ sessions.

As a consequence, other theories should use lib/ theories by session name,
not by path, which in turns means spec and proof sessions should also refer
to each other by session name, not path, to avoid duplicate theory errors in
theory merges later.

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/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

idle-thread-pd: run idle thread with the global PD all the time.

This avoids the multicore scenario of the idle thread running in the
address space that has been deleted by a thread running on another core.

x64: AInvs now done except ArchAInvsPre and KernelInit_AI

Isabelle2016-1: fix Word_Miscellaneous import path

This was previously missed, because Isabelle ignores the import path
when the file is already part of a loaded image.

Reported-by: Daniel Matichuk <Daniel.Matichuk@data61.csiro.au>

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>

x64: fix ARM build after merge

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: fix proofs involving UNION

SUPREMUM changed from a definition to an abbreviation.

A number of proofs that previously used blast, fastforce or auto to
solve goals involving UNION, now either fail or loop. This commit
includes various ad-hoc workarounds.

Isabelle2016-1: update references to renamed constants and facts

lib: move generic lemmas from AInvs to lib

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]

SELFOUR-64: Remove general Recycle operation

This removes the RecycleCap CNodeInvocation, whilst
retaining recycle behaviour for Endpoints -- now renamed
CNodeCancelBadgedSends.

autolevity: refine tracing apply everywhere to work via Proof module hooks

This avoids doing redundant tactic operations at the top-level and lets
us trace "by" statements easily.

lib: NonDetMonadLemmaBucket needs no words

lib/WordSetup: use the full Word_Lib entry

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

lib: start disentangling spaghetti word dependencies

cleanup for prod and when keyword

fix lib for isabelle 2016

fewer warnings

lib: Add a hoare_assume_pre variant for validNF.

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

Port AutoCorres to Isabelle 2014-RC0

Fix previous commit.

Move some more lemmas into lib.

release cleanup

Import release snapshot.