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

autocorres: remove Statistics and print_stats code

The “statistics” output has been disabled for some time, and the
print_stats option has never been part of the publicly documented
interface, so hopefully this removal will go unnoticed.

Some of the terms measured by the stats code are available through
the recently-added trace_* options (but not all).

autocorres: move new modules over the old ones

This is the “last” step of the Jira VER-517/VER-522 refactoring
(still does not support pausing between phases, but the relevant
infrastructure is there now).

Ought to pass AutoCorresTest suite now.

WIP: autocorres: start merging new code back into autocorres.ML

WIP: autocorres: VER-517 prototype for heap lifting

Heap lifting is annoying because we need to join all intermediate L2 results
before defining the lifted heap and proving heap lemmas.
This has been refactored into a new prepare_heap_lift stage that runs between
L2 conversion and HL proper.

WIP: autocorres: crude VER-517 prototypes for WA and TS phases

HL is still pending; the new code also needs to be refactored itself.

WIP: autocorres: split up function_info data structures

With this we move away from a global mutable fn_info; instead we will
use a table of persistent (lazy) entries for each phase.
Function call metadata is also now either stored locally or recomputed
on-demand for each stage (with a few TODOs).

WIP: autocorres: draft of more modular dependencies for L1, L2

Prototype for Jira VER-517.

autocorres: record all intermediate translation data

This allows us to perform incremental translation (VER-518) without
resorting to hacks.

word_lib: adjust theory dependencies

autocorres: add user option "no_c_termination" for previous patch.

Making termination proof optional for AutoCorres.

By default, the only change users will see is a new parameter to
ac_corres which will default to 'True'.

autocorres: fix skip_heap_abs option to actually skip all work.

autocorres: restore simplifier tracing functionality.

autocorres: rename "ccorres" predicate to "ac_corres".

This avoids a name conflict with the existing seL4 ccorres.

autocorres: 2015 update

more Isabelle2015 update; AInvs up to (excluding) Syscall_AI

also includes some global replacements

autocorres: Translate missing functions into constant "FUNCTION_BODY_NOT_IN_INPUT_C_FILE".

Functions that are declared in the C file, called by other C functions,
but are never actually _defined_ are translated simply into a "fail"
monadic statement. This sometimes causes confusion to new users.

We update AutoCorres to instead emit a new constant:

FUNCTION_BODY_NOT_IN_INPUT_C_FILE

defined simply as "fail" for such functions.

autocorres: experimental support for tracing heap_lift and word_abstract.

See tests/examples/TraceDemo.thy for an example.

autocorres: Move generic "set.ML" to "lib/" directory.

autocorres: Add "ptr_add_0_id" and "ptr_coerce.simps" back into the simpset.

These rules were removed because they are unhelpful for AutoCorres
internally, but remain generally useful for the end user.

autocorres: translate accesses to nested structs correctly. See tests/proof-tests/nested_struct.thy.

This should (finally) close issue JIRA VER-321. Unfortunately it also breaks some other things,
such as heap_abs_syntax, which we'll need to examine later.

Import release snapshot.