A Formalization of Metric Spaces in HOL Light

We present a computer formalization of metric spaces in the HOL Light theorem prover. Basic results of the theory of complete metric spaces are provided, including the Banach Fixed-Point Theorem, the Baire Category Theorem and the completeness of the space of continuous bounded functions. A decision procedure for a fragment of the elementary theory of metric spaces is also implemented. As an application, the Picard-Lindelof theorem on the existence of the solutions of ordinary differential equations is proved by using the well-known argument which appeals to the Banach theorem.