licenses: convert license tags to SPDX

global: isabelle update_cartouches

Isabelle2016-1: update to new ML API

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

more Isabelle2015 update; AInvs up to (excluding) Syscall_AI

also includes some global replacements

lib: Add experimental "distinct" command.

The "distinct" command takes a list of 'n' terms, and generates O(n^2)
lemmas for you to prove that the 'n' terms are all distinct. These
proofs can typically be carried out by an "apply auto" command, giving
you O(n^2) distinctness theorems.

These new theorems can then be thrown into a simpset to avoid having to
constantly unfold definitions merely to prove distinctness.

This brings quite significant speedups in the "Example_Valid_State"
proof (demonstrated in the next commit), for example, as it means that
raw definitions need not be unfolded, and hence automated tactics don't
get side-tracked with their numerical definitions.

The "distinct" command is not really scalable, due to its O(n^2) proof
terms generated. If we wanted to use this in a larger example, we would
probably want a "ordered" command, which forces you to show that 'n'
terms have some ordering, and then automatically derive the O(n^2)
possible proof terms on-the-fly in a simproc (possibly using Isabelle's
existing "order_tac").