Metric /

Filename Size Date modified Message
1.3 KB
1.3 KB
21.9 KB
2.2 KB
22.3 KB
1.0 KB
78.6 KB
11.6 KB
2.9 KB
2.0 KB
7.7 KB
                  Formalization of metric spaces in HOL Light
                     Copyright (c) 2014-2015 Marco Maggesi

The files in this folder contain a formalization of metric spaces for the HOL
Light theorem prover.

This code is now part of the HOL Light distribution (since svn revision 230
of 2015-05-17) with the exception of the file metricarith.hl.

The most important results proved in this formalization are the Contraction
Mapping Principle (also known as Banach Fixed-Point Theorem), the completeness
of the space of continuous bounded functions and the Baire Category theorem.

An implementation of a simple decision procedure for metric spaces, as
described in the paper

  R. M. Solovay, R. D. Arthan, J. Harrison
  "Some new results on decidability for elementary algebra and geometry"
  http://arxiv.org/abs/0904.3482

is also included.

As an application, we prove the Picard-Lindelöf theorem (or Cauchy-Lipschitz
theorem) about the existence of the solutions of ordinary differential
equations.

Part of this code is based on a previous work of Claudia Carapelle.  For
practical reasons, everything has been rewritten from scratch in order to
change certain implementation choices and for better adherence to the HOL Light
coding style.