Floating-point changes.

`fpX_to_value` is defined as `float_to_value o fpX_to_float` (previously this was called `fpX_to_real`, which was misleading)
`fpX_to_real` is now defined as `float_to_real o fpX_to_float`.

This change will break proofs that use the old names.

Make use of floating-point theorems from commit 4cb7d1f.

Add some floating-point theorems.

Theorems from the old floatTheory have been ported to the newer floating-point theory. The results have been generalised from being single precision only, allowing them to be instantiated to 16-, 32- and 64-bit floats.