small ints are now signed
define stateful inference system with full context

The context now may include any of the following kinds of things:
  type definition, constant specification,
  new type, new constant, or new axiom.

Define provability as a single relation (not in mutual recursion with
any others). Define terms/types in context, and well-formed contexts
(terms/types all ok in a linear sequence of context updates) separately.
Define semantics for HOL with full contexts

Semantics given using functions (no relations, no mutual recursion), and
interpretations of the theory context (in addition to the variable
valuations). Not 100% sure everything is right yet, but it's
well-commented and should be easy to audit.

Semantics in its own theory (i.e., aim to prove soundness/consistency in
a separate theory).
various tweaks to the HOL syntax and semantics

Use finite maps for the theory signature, to avoid the issue of
duplicate definitions. context_ok checks that the list of context
updates has no duplicates; to extract a signature from this list it is
turned into a finite map.

Also, give type abbreviations for various things that seem important:
assignments, valuations, signatures, interpretations... and clean up the
treatment of interpretations slightly.
some initial lemmas about the semantics

everything has become very context (signature) dependent. even though
the semantics aren't defined in terms of the signature, any proofs about
them require one to be around and the term/type to be good for that
signature. not sure if this is the right way to set things up...
prove termsem_equation, and more fiddling with the setup
prove some inference rules correct
prove the 8 easy inference rules correct

(the hard ones are INST, INST_TYPE, and the context-update rules)
(bad state) partial switch to using RDA's polymorphic values

also several lemmas about extending/reducing context, which motivated
this change. however, it seems like polymorphic values are probably a
mistake: we don't want term valuations to be general over type
valuations, since we actually always know what type valuation is
relevant. so, will probably go back to making being a term valuation
depend on a particular type valuation.

the other motivation for the change was to make type valuations
unconstrained on bad types (so a type valuation for an extended
signature is still a type valuation for any reduction of that signature:
it's allowed to send the undefined stuff anywhere). will keep this part
of the change.
revert polymorphic values, and prove new_const/new_type correct

these are the pure context updates that just add a new constant/type
operator to the context without defining them. essentially, have proved
that this is conservative.
prove new_axiom correct (after fixing it)

easy because we're concerned about validity of sequents in context:
we're allowed to assume all the axioms in the context hold, so adding a
new one doesn't make anything unproveable and lets you prove it too.

of course, we will also need at some point a result saying that certain
contexts actually do have models (e.g. if they only declare as axioms
the particular axioms we know how to prove are true)
work towards proving new_specification_correct

reduced to a cheat that looks to be just about the semantics of
substitution: probably worth proving INST correct first then re-using
the appropriate lemma.
Start working on semantics of subst/inst

Copy all the de Bruijn and freshly renamed terms stuff across, as well
as simple_inst and simple_subst, and prove a theorem about the semantics
of simple_subst. This actually involves a lot more code than Harrison's
original proofs (even though the results are basically the same): not
sure if it's worth it; the advantage is the proofs are somewhat less
complicated this way albeit more numerous.

This stuff is still really annoyingly fiddly, and a lot of it is because
of the stupid representation of substitutions/instantiations (as lists
of terms or types), and because there's not great support for updating
functions (unlike updating finite maps). I haven't switched to a better
representation (e.g. finite maps) this time, because I wanted to avoid
having to switch back and forth between them...
prove termsem_VSUBST and termsem_INST

the (proved) statement of the latter looks a bit worrying since it wants
to change to an interpretation of constants that ignores the type
valuation given to it...
prove INST_correct
simplify and strengthen termsem_INST

we don't need to assume the tyin only has variables in its domain.
attempt to prove INST_TYPE_correct, but looks false

or at least non-obvious: the problem is the term (constant) valuation
has changed and e.g. might not satisfy the axioms any more... need to
know that the change was benign, which I think means we need to
constrain term valuations more.
semi-major change: separate instance-matching from the constant assignment

this helps require constant assignments to be "uniform" on polymorphic
values. now the term semantics depends on the signature. this is closer
to what RDA has done, although it seems we need a small fix to his
approach to prevent constant assignments depending on irrelevant
valuations of type variables. holSoundnessScript.sml not updated in this
commit.
prove INST_TYPE_correct
alphabetise the order of the inferences in proves_rules