rework implementation of new_basic_type_definition and verify it

This almost completes verification of the monadic functions: the
remaining ones are new_constant, new_type, and new_axiom.

The implementation of the definition functions has diverged somewhat
from the original OCaml code because of our support for
new_specification as a primitive. This has knock-on effects on how
various helper functions work. In particular, add_constants and
add_types are used now to update the term/type references but not add
anything to the definitions reference.
minor cleanup
verify new_type, new_constant, and new_axiom

i.e. show that they preserve the refinement invariants.
this completes hol_verificationTheory, although later we might also want
to know that the implementation creates an analogue of hol_ctxt.