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).