reduce DRefine dependencies from Refine to AInvs

This needs (and includes) some deduplication and moving of lemmas formerly in
refine.

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

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

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/corres_method: update docs

lib/corres_method: bug fixes

* corres_pre now performs more conservative weakening
if the goal is already a corresK goal. This prevents
introducing a verification condition in the middle
of a proof.

* corres_inst_eq avoids splitting if statements when
unfolding corres_protect.

* corres_rv correctly handles schematic atomic postconditions
(previously would loop, now instiates them to True)

* corressimp fails on schematic goals to avoid looping

lib/corres_method: more robust schematics

corres method now fails outright if the subgoal
conclusion is schematic, otherwise it can loop.

Handle cases where corressimp
would leave preconditions uninstantiated if the
goal was solved by clarsimp.

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: misc bugfixes

Avoid introducing schematic assumption when corres preconditions
are concrete put stateless condition is schematic.

Avoid empty ruleset for corres_concrete_rER: causes corres to
loop unless it has at least one member.

lib/corres_method: mark more rules as corres_split

Since corres_splits rules are applied conservatively, we
can safely put the straightforward "corresK_if" rule in it,
leaving the reverse rule for corres_search.

Also "when" and "liftM" rules should be corres_splits,
rather than corresK, to handle cases where we might have
some more specific rule about a particular scenario and don't
necessarily want to unwrap the function.

lib/corres_method: add more conservative correswp

Correswp is wp but with more conservative treatment for
schematics. Rules in wp_comb that do precondition weakening
are avoided when the precondition is schematic, and there
is a final check which fails if any schematic preconditions
are found.

Realistically this should be the default behaviour for wp, but
that's a potentially bigger change.

lib/corres_method: better lift_corres_args

Handles multiple arguments and fails if no arguments are lifted

lib/corres_method: misc tuning

lib/corres_method: remove simp step from corres

Instead of doing rewriting corres should only rely on
rule application to ensure it only manipulates the
head function (and only if such manipulation causes
corres progress to be made).

lib/corres_method: generalize assumption protection

Generated goal premises (i.e. from bind or if split rules)
should in most cases be redundant, as necessary conditions can
simply be propagated. By aggressively protecting them, we afford
ourselves greater control over how function bodies are rewritten.

lib/corres_method: ex_abs -> ex_abs_underlying

ex_abs appears later in Refine so it can just be
rephrased as an abbreviation

lib/corres_method: unfold protect_r in corressimp

Allow corressimp to use the return-value relation in its clarsimp step
if doing so allows it to solve the subgoal.

This addresses some occasions where wp generates in-place goals that can
be easily solved (rather than pushing them into preconditions).

lib/corres_method: misc cleanup

lib/corres_method: speed up corresc

This avoids any backtracking when solving the contradictions
emerging from left/right case splitting. Should result in 2-3x
speedup in some cases.

lib/corres_method: add const for instantiation

Some schematic instantiations require knowledge from return-value
relations. The special const "corres_eq_inst" indicates to corres
that a schematic instantiation should be possible/obvious by
unfolding the protected assumptions and applying fastforce.

lib/corres_method: add better corres_rv rules

lib/corres_method: hide return relation

Protect the return value relation by default so we can control
the simplifier.

lib/corres_method: add corres to wp lifting rules

lib/corres_method: add better corres_rv rules

x64: progress in VSpace_R

Corres lemmas are proven. Remaining:
- A handfull of Hoare triples.
- The Haskell spec for invalidateASID needs to be updated
to close a small hole in each of unmap_pd_corres and
unmap_pdpt_corres.

x64 refine: fix Retype_R

Also:
- Design spec and haskell invariants fixes.
- Moves corresK rules for mapM and mapM_x into Corres_Method.

corres_method: remove corres_concrete_P, reorder preconditions

Prefer to solve corres_rv/stateless preconditions first. This
lets them easily be introduced as assumptions with context_conjI.

corres_method: don't add F to goal prems

This causes too much unintentional simplification.

corres_method: major overhaul to use corres_underlyingK

This gives the corres method its own calculus where it has better
control over additional rule assumptions.

corres_method: add right-hand variant of normal_corres

This allows stateless preconditions to propagate from the
right (concrete) side rather than the left side as usual.

corres_method: more careful treatment of schematics

This adds new classes of corres rules which require different
goal parameters to be instantiated. corressimp avoids applying
wp or simp rules which would expose schematics.

corres_method: invoke corresc from corres

This is done so that "corres_once" will consider it a successful
application if it manages to perform a case split.

corres_method: better symbolic execution support

- Abstract symbolic execution theorems into named_theorems
- More rules for error monad

corres_method: use corres method by default

corres_method: edge case with corres_search

Handle case where corres_search requires no searching at all.

corres_method: avoid unnecessary goal restriction

This makes traces a bit more readable

corres_method: add breakpoints

fixed algorithm for corres_search

added Corres_Test theory file with example proofs from VSpace_R

initial commit for corres method (experimental)