Implement conversion from HOL4 to OpenTheory numerals

Use HOL4's definitions of inv and / in the hol-real package

Because they are overspecified (in particular, defined for 0 as
divisor), they cannot be mapped directly to the underspecified
OpenTheory versions. However, we can prove they are equal to the
OpenTheory versions for all other inputs.

Add interpretation of real constants to hol4.int

sup is not included because the type is different in OpenTheory (set
versus predicate)

Split out and re-use HOL interpretation

OpenTheory now supports importing an interpretation from a file.