Formalization of Fixed-Point Arithmetic in HOL