lib: Isabelle2020 update

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX

lib: update for Isabelle 2019

lib: fix up Levity dependency tracking

Uses proof body terms to disambiguate the names encoutered in
dependency extraction, rather than using (for example)
Thm.full_prop_of.

The result is that this catches a few more missing dependencies,
enough to correctly identify unused lemmas large sessions
like CRefine.

lib: fix up Levity JSON output

- Previously printed `~` for negative numbers, which is invalid
JSON. Now prints `-`.

- Previously the outpout would unconditionally trim
'underscore-number' suffixes. Now uses theory context to determine
if it's likely to be an index into a theory list or an existing
fact name.

- Changed JSON structure to avoid using dynamic names for keys, i.e.
from this:

{
"my_theory_name": {...}
}

to this:

{
"theory": "my_theory_name",
"content": {...}
}

This should make processing the output slightly nicer by matching
what other tools expect.

- Changed JSON structure to consolidate dependencies. Lemmas are no
longer special-cased.

Isabelle2017: update lib for RC0

* ML Proof_Context.fact_alias renamed to alias_fact.

* Named_Target.init removed redundant parameter.

* Simplified Greatest, removed GreatestM.

* Introduced thm_node type in proofterm.ML.

Removes all trailing whitespaces

Isabelle2016-1: update to new ML API

Update references to renamed ML constants; supply default arguments to
functions with additional parameters; etc.

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.

autolevity: add support for per-apply lemma dependency tracking

Also remove at-end theory hook due to unfinished proofs causing issues. Autolevity must be run from a completed session (see lib/AutoLevity_Run).

Per-apply dependency tracking requires a small isabelle patch.

autolevity: avoid emitting ~1 subgoals in corner cases

autolevity: initial commit with test run on AInvs