Isabelle2018: Lib update

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

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

lib: repair WPTutorial and CorresTest

Parts of CorresTest don't work any more after changes to the underlying
example functions.

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/corres_method: tuning and documentation

lib/corres_method: method for corres_rv

This removes corres_choice in favour of making corres_rv smarter.
Now corres_rv can propagate a stateless condition, and the new
corres_rv method (called from corres) tries to push the generated
obligation into the appropriate place (stateless, left or right
precondition) based on which variables it discusses.

This avoids most cases where the corres_rv_wp_left/right or
corres_rv_defer rules needed to be specified manually.

lib/corres_method: careful treatment for schematics

The new "corres_choice_true" and "corres_choice_false" constants
represent a deferred choice for how to propagate a generated
stateless precondition. If possible, we would prefer to do so
via the outermost stateless precondition, since it has access
to all green variables. Importantly corres_rv_defer_left/right
are subsumed by the more general corres_rv_defer.

Also we introduce alternative wp_comb rules which introduce
a corres_inst_eq goal, rather than a raw meta-implication. This
is to avoid cases where the existing wp_comb methods would incorrectly
introduce schematic assumptions, resulting in unprovable goals. This
allows for more carefully controlling unification in cases where
the precondition of a hoare triple doesn't have access to all
necessary green variables.

lib/corres_method: fix test for latest method

lib/corres_method: repair Corres_Test after changes

corres_method: add some documentation

Fixup proofs for test theory

corres_method: update Corres_Test for new corresK

apply_debug steps now slightly different, different
verification condition.

corres_method: use apply_debug by default

corres_method: add traces for corres method tests

fixed algorithm for corres_search

added Corres_Test theory file with example proofs from VSpace_R